proposition: Lemma homography : forall (a b c d : Z) (s : Q) (H_Qhomographic_denom_nonzero : Qhomographic_denom_nonzero c d s), Qhomographic a b c d s H_Qhomographic_denom_nonzero = spec_h a b c d s.
proof: Proof. intros a b c d [| s| s] H_Qhomographic_denom_nonzero. unfold Qhomographic in |- *. unfold spec_h in |- *. rewrite Qmult_sym with a Zero. rewrite Qmult_sym with c Zero. repeat rewrite Qmult_zero. repeat rewrite Qplus_zero_left. rewrite coding_Q. reflexivity. unfold Qhomographic in |- *. unfold spec_h in |- *. apply homography_positive_input. unfold Qhomographic in |- *. unfold spec_h in |- *. rewrite homography_positive_input. apply f_equal2 with Q Q; [ idtac | apply f_equal with Q ]; apply f_equal2 with Q Q; trivial; repeat rewrite Z_to_Qopp; repeat rewrite <- Qmult_neg; abstract ring. Defined.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)