proposition: Lemma gcd_greatest a b c : (c|a) -> (c|b) -> (c | gcd a b).
proof: Proof. assert (H : forall p q r, (r|pos p) -> (r|pos q) -> (r|pos (Pos.gcd p q))). { intros p q [|r|r] H H'. - destruct H; now rewrite mul_comm in *. - apply divide_Zpos, Pos.gcd_greatest; now apply divide_Zpos. - apply divide_Zpos_Zneg_l, divide_Zpos, Pos.gcd_greatest; now apply divide_Zpos, divide_Zpos_Zneg_l. } destruct a, b; simpl; auto; intros; try apply H; trivial; now apply divide_Zpos_Zneg_r. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass