proposition: Lemma Ngcd_sum a b: natp a -> natp b -> Ngcd a (a +c b) = Ngcd a b.
proof: Proof. move => aN bN; rewrite - {2} (cprod1r (CS_nat aN)) csumC. apply: (Ngcd_rem aN bN NS1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)