proposition: Lemma Qquadratic_Qpositive_to_Qpositive_1 : forall (a b c d e f g h : Z) (p1 p2 : Qpositive) (hyp : quadraticAcc a b c d e f g h p1 p2), p1 <> One -> p2 <> One -> quadratic_top_more a b c d e f g h -> forall hyp_rec : quadraticAcc (a - e) (b - f) (c - g) (d - h) e f g h p1 p2, Qquadratic_Qpositive_to_Qpositive a b c d e f g h p1 p2 hyp = nR (Qquadratic_Qpositive_to_Qpositive (a - e) (b - f) (c - g) (d - h) e f g h p1 p2 hyp_rec).
proof: Proof. intros. apply trans_eq with (Qquadratic_Qpositive_to_Qpositive a b c d e f g h p1 p2 (quadraticacc1 a b c d e f g h p1 p2 H H0 H1 hyp_rec)). apply Qquadratic_Qpositive_to_Qpositive_equal. unfold Qquadratic_Qpositive_to_Qpositive;fold Qquadratic_Qpositive_to_Qpositive; case (Qpositive_dec_One p1); intros Hp1; [ Falsum | idtac ]; case (Qpositive_dec_One p2); intros Hp2; [ Falsum | idtac ]; case (quadratic_top_more_informative a b c d e f g h); intros Habcdefgh; [ idtac | Falsum ]; apply f_equal with Qpositive; reflexivity. Qed.
imports: QArithSternBrocot(Merge_Order)