proposition: Lemma Ngcd_P a b: natp a -> natp b -> (Ngcd_prop a b (Ngcd a b) /\ forall g, Ngcd_prop a b g -> (Ngcd a b) = g).
proof: Proof. move => aN bN. move:(BZ_of_nat_i aN)(BZ_of_nat_i bN) => az bz. move:(NS_gcd aN bN) => gN. have ww: BZ_of_nat (Ngcd a b) = BZgcd (BZ_of_nat a) (BZ_of_nat b). apply:(BZp_hi_pr (ZpS_gcd az bz)). move:(BZgcd_prop3' az bz) => [[ha hb hc hd] he]. have: Ngcd a b %|c a by apply/(BZdiv_cN gN aN); rewrite ww. have: Ngcd a b %|c b by apply/(BZdiv_cN gN bN); rewrite ww. have Hp t: natp t -> t %|c a -> t %|c b -> t %|c Ngcd a b. move => tN /(BZdiv_cN tN aN) sa /(BZdiv_cN tN bN) sb. by apply /(BZdiv_cN tN gN); rewrite ww; apply:hd => //; apply: BZ_of_natp_i. split => // k [ga gb gc gd]. apply/BZ_of_nat_inj; rewrite ww; apply: he; split. + by apply: BZ_of_natp_i. + by apply/BZdiv_cN. + by apply/BZdiv_cN. + move => y tp;move:(BZ_valN (BZp_sBZ tp)) => h. move: (BZp_hi_pr tp) => <- /(BZdiv_cN h aN) sa /(BZdiv_cN h bN) sb. by apply /(BZdiv_cN h ga); apply: gd. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)