proposition: Lemma nat_prime_coprime a b: nat_prime a -> nat_prime b -> a = b \/ coprime a b.
proof: Proof. move => [aN ag1 ap] [bN bg1 bp]. case: (equal_or_not a b) => eab; [by left | right; split => //]. move => x xda xdb. move:(cdivides_pr xda) (cdivides_pr xdb) => ea eb. case:(ap _ _ (proj32 xda) (NS_quo x aN) ea) => // => ec. case:(bp _ _ (proj32 xdb) (NS_quo x bN) eb) => // => ed. by case: eab; rewrite ea eb ec ed. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)