proposition: Lemma Qgcd_pos_divides (a b: Qpos): exists c: positive, inject_Z c * proj1_sig (Qcd_pos a b) == proj1_sig a.
proof: Proof. Proof with auto with *. revert a b. intros [a ap] [b bp]. simpl. destruct (Qgcd_divides a b) as [x E]. destruct x. exfalso. ring_simplify in E. revert ap. rewrite E. apply Qlt_irrefl. exists p... exfalso. rewrite <- E in ap. apply (Qlt_irrefl 0). apply Qlt_le_trans with (inject_Z (Zneg p) * Qgcd a b)... rewrite Qmult_comm. apply Qmult_nonneg_nonpos... Qed.
imports: Coq.QArith.QArith CoRN.model.Zmod.ZGcd CoRN.model.totalorder.QposMinMax CoRN.stdlib_omissions.Q