proposition: Lemma gcdn_gt0 m n : (0 < gcdn m n) = (0 < m) || (0 < n).
proof: Proof. by case: m n => [|m] [|n] //; apply: (@dvdn_gt0 _ m.+1) => //; apply: dvdn_gcdl. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)