proposition: Lemma homography_positive_input : forall (a b c d : Z) (p : Qpositive) (H_Qhomographic_sg_denom_nonzero : Qhomographic_sg_denom_nonzero c d p), Qhomographic_Qpositive_to_Q 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. functional induction (Qhomographic_Qpositive_to_Q a b c d p H_Qhomographic_sg_denom_nonzero). clear e0 e3 e2. rename x into Hc0; rename e into ad_eq_bc; rewrite coding_Q. assert (b0_eq_zero : b = 0%Z). rewrite Zmult_0_r in ad_eq_bc. apply Zmult_integral_l with c;assumption || symmetry in |- *; assumption. rewrite b0_eq_zero. simpl in *. unfold spec_fraction_encoding in |- *; repeat rewrite Qplus_zero_right; abstract ( rewrite <- Qdiv_num_denom; [ reflexivity | discriminate ]) . clear e0 e2 e3. rename x into Hc0; rename e into ad_eq_bc; rewrite coding_Q. assert (b0_eq_zero : b = 0%Z). rewrite Zmult_0_r in ad_eq_bc. apply Zmult_integral_l with c;assumption || symmetry in |- *; assumption. rewrite b0_eq_zero. simpl in *. unfold spec_fraction_encoding in |- *; repeat rewrite Qplus_zero_right; abstract ( rewrite <- Qdiv_num_denom; [ reflexivity | discriminate ]) . rewrite coding_Q; unfold spec_fraction_encoding in |- *; symmetry in |- *; apply a_field_equality_1; [ repeat rewrite <- Z_to_Qmult; apply f_equal with Z | replace Zero with (Z_to_Q 0); trivial; apply Z_to_Q_not_eq | apply Qhomographic_sg_denom_nonzero_correct_1 ]; assumption. clear e0 e; symmetry in |- *; replace (Qmult (Qplus (Qmult a (Qpos p)) b) (Qinv (Qplus (Qmult c (Qpos p)) d))) with (spec_Qhomographic_Qpositive_to_Q a b c d p); trivial; apply Qsgn_2; rewrite <- (homographic_sign a b c d p H_Qhomographic_sg_denom_nonzero); assumption. rewrite output_bit; rewrite <- spec_Qhomographic_Qpositive_to_Q_spec_ni2_pos; unfold spec_Qhomographic_Qpositive_to_Q in |- *; rewrite sg_pres_fraction; [ reflexivity | change (Qsgn (spec_Qhomographic_Qpositive_to_Q a b c d p) = 1%Z) in |- *; rewrite <- (homographic_sign a b c d p H_Qhomographic_sg_denom_nonzero); assumption ]. rewrite output_bit; rewrite <- spec_Qhomographic_Qpositive_to_Q_spec_ni2_pos; rewrite spec_Qhomographic_Qpositive_to_Q_Zopp; unfold spec_Qhomographic_Qpositive_to_Q in |- *; rewrite sg_pres_fraction; [ reflexivity | change (Qsgn (spec_Qhomographic_Qpositive_to_Q a b c d p) = 1%Z) in |- *; rewrite <- (homographic_sign a b c d p H_Qhomographic_sg_denom_nonzero); assumption ]. rewrite output_bit; rewrite <- spec_Qhomographic_Qpositive_to_Q_spec_ni2_neg_1; unfold spec_Qhomographic_Qpositive_to_Q in |- *; rewrite sg_pres_fraction; [ reflexivity | change (Qsgn (spec_Qhomographic_Qpositive_to_Q a b c d p) = (-1)%Z) in |- *; rewrite <- (homographic_sign a b c d p H_Qhomographic_sg_denom_nonzero); assumption ]. rewrite output_bit; rewrite <- spec_Qhomographic_Qpositive_to_Q_spec_ni2_neg_2; unfold spec_Qhomographic_Qpositive_to_Q in |- *; rewrite sg_pres_fraction; [ reflexivity | change (Qsgn (spec_Qhomographic_Qpositive_to_Q a b c d p) = (-1)%Z) in |- *; rewrite <- (homographic_sign a b c d p H_Qhomographic_sg_denom_nonzero); assumption ]. Defined.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)