Commit 171c94fa authored by MARCHE Claude's avatar MARCHE Claude

Missing file added

Ca m'apprendra a commiter/pusher trop vite...
parent 056832f1
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require Import ZOdiv.
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.
(* Why3 assumption *)
Definition coprime (a:Z) (b:Z): Prop := ((number.Gcd.gcd a b) = 1%Z).
Lemma coprime_is_Zrel_prime :
forall a b, coprime a b <-> Znumtheory.rel_prime a b.
unfold coprime.
unfold Znumtheory.rel_prime.
split; intro h.
rewrite <- h; apply Znumtheory.Zgcd_is_gcd.
apply Znumtheory.Zis_gcd_gcd; auto with zarith.
(* Why3 goal *)
Lemma prime_coprime : forall (p:Z), ( p) <->
((2%Z <= p)%Z /\ forall (n:Z), ((1%Z <= n)%Z /\ (n < p)%Z) -> (coprime n
intros p.
forall p : int,
(1 < p)%Z ->
(forall n : int, (1 <= n < p)%Z -> Znumtheory.rel_prime n p) -> p
rewrite Prime.prime_is_Zprime.
intro h; inversion h; clear h.
split; auto with zarith.
intros n h.
rewrite coprime_is_Zrel_prime.
apply H0; auto.
intros (h1,h2).
constructor; auto with zarith.
intros n h.
rewrite <- coprime_is_Zrel_prime.
apply h2; auto.
(* Why3 goal *)
Lemma Gauss : forall (a:Z) (b:Z) (c:Z), ((number.Divisibility.divides a
(b * c)%Z) /\ (coprime a b)) -> (number.Divisibility.divides a c).
intros a b c (h1,h2).
apply Znumtheory.Gauss with b; auto.
rewrite <- coprime_is_Zrel_prime; auto.
(* Why3 goal *)
Lemma Euclid : forall (p:Z) (a:Z) (b:Z), (( p) /\
(number.Divisibility.divides p (a * b)%Z)) -> ((number.Divisibility.divides
p a) \/ (number.Divisibility.divides p b)).
intros p a b (h1,h2).
apply Znumtheory.prime_mult; auto.
now rewrite <- Prime.prime_is_Zprime.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment