proposition: Lemma Ngcd_rem a b q: natp a ->natp b -> natp q -> Ngcd a (b +c a *c q) = Ngcd a b.
proof: Proof. move => aN bN qN. rewrite /Ngcd - (BZsum_cN bN (NS_prod aN qN)) - (BZprod_cN aN qN). by rewrite BZgcd_rem //; apply: BZ_of_nat_i. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)