proposition: Lemma Ngcd_div a b (g:= (Ngcd a b)): natp a -> natp b -> a = g *c (a %/c g) /\ b = g *c (b %/c g).
proof: Proof. move => aN bN. move:(BZ_of_nat_i aN)(BZ_of_nat_i bN) => az bz. move: (BZp_hi_pr (ZpS_gcd az bz)) (BZ_valN (ZS_gcd az bz)) (BZgcd_div az bz). move => eq hh. set h := (P (BZgcd (BZ_of_nat a) (BZ_of_nat b))). move: (NS_quo h aN) (NS_quo h bN) => caN cbN. rewrite - eq (BZquo_cN aN hh) (BZquo_cN bN hh) (BZprod_cN hh caN). rewrite (BZprod_cN hh cbN); move => [/BZ_of_nat_inj aa /BZ_of_nat_inj bb]. done. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)