proposition: Lemma Qquadratic_Qpositive_to_Qpositive_0' : 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 -> forall hyp_ni : homographicAcc (a + b) (c + d) (e + f) (g + h) p1, Qquadratic_Qpositive_to_Qpositive a b c d e f g h p1 p2 hyp = Qhomographic_Qpositive_to_Qpositive (a + b) (c + d) (e + f) (g + h) p1 hyp_ni.
proof: Proof. intros. apply trans_eq with (Qquadratic_Qpositive_to_Qpositive a b c d e f g h p1 One (quadraticacc0' a b c d e f g h p1 One H (refl_equal One) hyp_ni)). apply Qquadratic_Qpositive_to_Qpositive_equal_strong; reflexivity || assumption. unfold Qquadratic_Qpositive_to_Qpositive;fold Qquadratic_Qpositive_to_Qpositive; case (Qpositive_dec_One p1); intros Hp1; [ Falsum | idtac ]; reflexivity. Qed.
imports: QArithSternBrocot(Merge_Order)