proposition: Lemma spec_Qhomographic_Qpositive_to_Q_nR_unfolded : forall (a b c d : Z) (q : Qpositive), Qmult (Qplus (Qmult a (Qpos (nR q))) b) (Qinv (Qplus (Qmult c (Qpos (nR q))) d)) = Qmult (Qplus (Qmult a (Qpos q)) (a + b)%Z) (Qinv (Qplus (Qmult c (Qpos q)) (c + d)%Z)).
proof: Proof. Proof spec_Qhomographic_Qpositive_to_Q_nR. Lemma spec_Qhomographic_Qpositive_to_Q_dL_unfolded : forall (a b c d : Z) (q : Qpositive), Qmult (Qplus (Qmult a (Qpos (dL q))) b) (Qinv (Qplus (Qmult c (Qpos (dL q))) d)) = Qmult (Qplus (Qmult (a + b)%Z (Qpos q)) b) (Qinv (Qplus (Qmult (c + d)%Z (Qpos q)) d)). Proof spec_Qhomographic_Qpositive_to_Q_dL. Lemma spec_ni2_nR : forall (a b c d : Z) (q : Qpositive), spec_ni2 a b c d (nR q) = spec_ni2 a (a + b) c (c + d) q. Proof. intros. unfold spec_ni2 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)