proposition: Lemma Ngcd_diff a b: natp a -> natp b -> a <=c b -> Ngcd a (b -c a) = Ngcd a b.
proof: Proof. move => aN bN le1. rewrite - {2} (cdiff_pr le1); symmetry; apply:(Ngcd_sum aN (NS_diff a bN)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)