proposition: Lemma Qquadratic_Qpositive_to_Q_3 : forall (a b c d e f g h : Z) (p1 p2 : Qpositive) (H_Qquadratic_sg_denom_nonzero : Qquadratic_sg_denom_nonzero e f g h p1 p2) (He : e <> 0%Z), same_ratio a b c d e f g h -> Qquadratic_Qpositive_to_Q a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero = fraction_encoding a e He.
proof: Proof. intros a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero. functional induction (Qquadratic_Qpositive_to_Q a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero); intros; try solve [ Falsum ]; match goal with [ id:same_ratio _ _ _ _ _ _ _ _ |- _] => elim id; intros h1 (h2, (h3, (h4, (h5, h6)))); apply fraction_encoding_reduces; trivial; symmetry in |- *; assumption end. Qed.
imports: Coq(FunInd) QArithSternBrocot(homographic_correctness)