proposition: Lemma Qpos_gcd3 (a b c: Qpos): exists g: Qpos, exists i: positive, inject_Z i * proj1_sig g == proj1_sig a /\ exists j: positive, inject_Z j * proj1_sig g == proj1_sig b /\ exists k: positive, inject_Z k * proj1_sig g == proj1_sig c.
proof: Proof. Proof with auto. intros. exists (Qcd_pos a (Qcd_pos b c)). destruct (Qgcd_pos_divides b c) as [x E]. destruct (Qgcd_pos_divides c b) as [x0 F]. simpl in F. rewrite Qgcd_sym in F. change (inject_Z x0 * proj1_sig (Qcd_pos b c) == proj1_sig c) in F. revert E F. generalize (Qcd_pos b c). intros. destruct (Qgcd_pos_divides a q) as [x1 G]. destruct (Qgcd_pos_divides q a) as [x2 H]. simpl in H. rewrite Qgcd_sym in H. change (inject_Z x2 * proj1_sig (Qcd_pos a q) == proj1_sig q) in H. exists x1. revert G H. generalize (Qcd_pos a q). split... exists (x * x2)%positive. split. rewrite Q.Pmult_Qmult. rewrite <- Qmult_assoc. rewrite H... exists (x0 * x2)%positive. rewrite Q.Pmult_Qmult. rewrite <- Qmult_assoc. rewrite H... Qed.
imports: Coq.QArith.QArith CoRN.model.Zmod.ZGcd CoRN.model.totalorder.QposMinMax CoRN.stdlib_omissions.Q