proposition: Lemma Qgcd_nonneg a b: 0 <= Qgcd a b.
proof: Proof. revert a b. intros [an ad] [bn bd]. simpl. unfold Qle. simpl. auto with *. Qed.
imports: Coq.QArith.QArith CoRN.model.Zmod.ZGcd CoRN.model.totalorder.QposMinMax CoRN.stdlib_omissions.Q