proposition: Lemma Ngcd_nz a b: natp a -> natp b -> Ngcd a b = \0c -> (a = \0c /\ b = \0c).
proof: Proof. by move => az bz h; move: (Ngcd_div az bz); rewrite h !cprod0l. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)