proposition: Lemma spec_Qhomographic_Qpositive_to_Q_nR : forall (a b c d : Z) (q : Qpositive), spec_Qhomographic_Qpositive_to_Q a b c d (nR q) = spec_Qhomographic_Qpositive_to_Q a (a + b) c (c + d) q.
proof: Proof. intros. unfold spec_Qhomographic_Qpositive_to_Q in |- *. do 2 rewrite Qmult_Z_nR. repeat rewrite <- Qplus_assoc. repeat rewrite <- Z_to_Qplus. reflexivity. Defined.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)