proposition: Lemma spec_ni2_dL : forall (a b c d : Z) (q : Qpositive), Qplus (Qmult (a + b)%Z (Qpos q)) b <> Zero -> Qplus (Qmult (c + d)%Z (Qpos q)) d <> Zero -> spec_ni2 a b c d (dL q) = spec_ni2 (a + b) b (c + d) d q.
proof: Proof. intros a b c d p Hnum Hdenom. unfold spec_ni2 in |- *. do 2 rewrite Qmult_Z_plus_Z_dL. repeat rewrite <- Q_tail_Qinv. repeat rewrite <- Q_tail_Qmult; try assumption. apply f_equal with Q. rewrite <- Qdiv_num_denom; [ reflexivity | discriminate ]. apply Qinv_resp_nonzero; assumption. apply Qmult_resp_nonzero; [ assumption | discriminate ]. apply Qinv_resp_nonzero; apply Qmult_resp_nonzero; [ assumption | discriminate ]. Defined.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)