proposition: Lemma sg_pres_fraction : forall (a b c d : Z) (p : Qpositive) (H_Qhomographic_sg_denom_nonzero : Qhomographic_sg_denom_nonzero c d p), Qmult (Qplus (Qmult (new_a a b c d p H_Qhomographic_sg_denom_nonzero) (Qpos (new_p a b c d p H_Qhomographic_sg_denom_nonzero))) (new_b a b c d p H_Qhomographic_sg_denom_nonzero)) (Qinv (Qplus (Qmult (new_c a b c d p H_Qhomographic_sg_denom_nonzero) (Qpos (new_p a b c d p H_Qhomographic_sg_denom_nonzero))) (new_d a b c d p H_Qhomographic_sg_denom_nonzero))) = Qmult (Qplus (Qmult a (Qpos p)) b) (Qinv (Qplus (Qmult c (Qpos p)) d)).
proof: Proof. intros a b c d p H_Qhomographic_sg_denom_nonzero. unfold new_a, new_b, new_c, new_d, new_p in |- *. functional induction (Qhomographic_sign a b c d p H_Qhomographic_sg_denom_nonzero); try reflexivity;rewrite IHp0; clear IHp0;symmetry in |- *; try first [ apply spec_Qhomographic_Qpositive_to_Q_nR_unfolded | apply spec_Qhomographic_Qpositive_to_Q_dL_unfolded ]. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)