proposition: Lemma gcd_greatest a b c : (c|a) -> (c|b) -> (c|gcd a b).
proof: Proof. destruct a as [ |p], b as [ |q]; simpl; trivial. destruct c as [ |r]. - intros (s,H). destruct s; discriminate. - intros ([ |s],Hs) ([ |t],Ht); try discriminate; simpl in *. destruct (Pos.gcd_greatest p q r) as (u,H). + exists s. now inversion Hs. + exists t. now inversion Ht. + exists (pos u). simpl; now f_equal. Qed.
imports: BinNums BinPos RelationClasses Morphisms Setoid Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties