proposition: Lemma Qgcd_sym (a b: Q): Qgcd a b = Qgcd b a.
proof: Proof. unfold Qgcd. intros. rewrite Zgcd_nat_sym. rewrite Pmult_comm. reflexivity. Qed.
imports: Coq.QArith.QArith CoRN.model.Zmod.ZGcd CoRN.model.totalorder.QposMinMax CoRN.stdlib_omissions.Q