(* This file is generated by Why3's Coq driver *) (* Beware! Only edit allowed sections below *) Require Import BuiltIn. Require BuiltIn. Require int.Int. Require int.Abs. Require int.EuclideanDivision. Require int.ComputerDivision. Require number.Parity. Require number.Divisibility. Require number.Gcd. Require number.Prime. Require number.Coprime. (* Why3 assumption *) Definition lt_nat (x:Z) (y:Z): Prop := (0%Z <= y)%Z /\ (x < y)%Z. (* Why3 assumption *) Inductive lex: (Z* Z)%type -> (Z* Z)%type -> Prop := | Lex_1 : forall (x1:Z) (x2:Z) (y1:Z) (y2:Z), (lt_nat x1 x2) -> (lex (x1, y1) (x2, y2)) | Lex_2 : forall (x:Z) (y1:Z) (y2:Z), (lt_nat y1 y2) -> (lex (x, y1) (x, y2)). Axiom even1 : forall (n:Z), (0%Z <= n)%Z -> ((number.Parity.even n) <-> (n = (2%Z * (ZArith.BinInt.Z.quot n 2%Z))%Z)). Axiom odd1 : forall (n:Z), (0%Z <= n)%Z -> ((~ (number.Parity.even n)) <-> (n = ((2%Z * (ZArith.BinInt.Z.quot n 2%Z))%Z + 1%Z)%Z)). Axiom div_nonneg : forall (n:Z), (0%Z <= n)%Z -> (0%Z <= (ZArith.BinInt.Z.quot n 2%Z))%Z. Axiom gcd_even_even : forall (u:Z) (v:Z), (0%Z <= v)%Z -> ((0%Z <= u)%Z -> ((number.Gcd.gcd (2%Z * u)%Z (2%Z * v)%Z) = (2%Z * (number.Gcd.gcd u v))%Z)). (* Why3 goal *) Theorem gcd_even_odd : forall (u:Z) (v:Z), (0%Z <= v)%Z -> ((0%Z <= u)%Z -> ((number.Gcd.gcd (2%Z * u)%Z ((2%Z * v)%Z + 1%Z)%Z) = (number.Gcd.gcd u ((2%Z * v)%Z + 1%Z)%Z))). (* Why3 intros u v h1 h2. *) intros u v h1 h2. rewrite Gcd.Comm. rewrite number.Coprime.gcd_coprime. now rewrite Gcd.Comm. unfold Coprime.coprime. rewrite <- Gcd.Gcd_computer_mod; auto with zarith. rewrite ComputerDivision.Mod_mult; auto with zarith. Qed.