proposition: Lemma spec_Qhomographic_Qpositive_to_Q_dL : forall (a b c d : Z) (q : Qpositive), spec_Qhomographic_Qpositive_to_Q a b c d (dL q) = spec_Qhomographic_Qpositive_to_Q (a + b) b (c + d) d q.
proof: Proof. intros. unfold spec_Qhomographic_Qpositive_to_Q in |- *. do 2 rewrite Qmult_Z_plus_Z_dL. set (p := Qpos q) in *. set (A := Z_to_Q (a + b)) in *. set (C := Z_to_Q (c + d)) in *. rewrite <- Qdiv_num_denom. reflexivity. discriminate. Defined.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)