proposition: Lemma square_increase_rev : forall O E E' A B A2 B2, Ps O E A -> Ps O E B -> LtP O E E' A2 B2 -> Prod O E E' A A A2 -> Prod O E E' B B B2 -> LtP O E E' A B.
proof: Proof. intros. assert(HP2:= H2). assert(HP3:=H3). unfold Prod in HP2. unfold Prod in HP3. spliter. unfold Ar2 in *. spliter. clean_duplicated_hyps. clear H7 H5. assert(HS:=sum_exists O E E' H6 B A H8 H11). ex_and HS SS. assert(HD:= diff_exists O E E' B A H6 H8 H11). ex_and HD DD. assert(exists C : Tpoint, Prod O E E' SS DD C). { apply(prod_exists O E E' H6 SS DD). unfold Sum in H4. unfold Ar2 in H4. tauto. unfold Diff in H5. ex_and H5 X. unfold Sum in H7. spliter. unfold Ar2 in H7. tauto. } ex_and H7 PSD. assert(HH:= diff_exists O E E' B2 A2 H6 H10 H13). ex_and HH D2. assert(HH:= diff_of_squares O E E' B A B2 A2 D2 SS DD PSD H3 H2 H7 H4 H5 H9). subst PSD. assert(HH:=(ltp__diff_pos O E E' A2 B2 D2 H1 H7)). apply(prod_pos__signeq) in H9; auto. unfold SignEq in H9. induction H9. { spliter. apply diff_pos__ltp in H5; auto. } { spliter. apply False_ind. assert(HS:= sum_pos_pos O E E' B A SS H0 H H4). apply pos_not_neg in HS. contradiction. } intro. subst SS. apply sum_pos_pos in H4; auto. unfold Ps in H4. unfold Out in H4. tauto. intro. subst DD. apply diff_null_eq in H5. subst B. assert(Prod O E E' SS O O). { apply (prod_0_r O E E' SS). Col. unfold Sum in H4. unfold Ar2 in H4. spliter; tauto. } assert(D2 = O). { apply (prod_uniqueness O E E' SS O); auto. } subst D2. assert(B2 = A2). { apply(diff_null_eq O E E'); auto. } subst B2. unfold LtP in H1. ex_and H1 DF. assert(HD:= diff_null O E E' A2 H6 H13). assert(DF=O). { apply(diff_uniqueness O E E' A2 A2); auto. } subst DF. unfold Ps in H12. unfold Out in H12. tauto. Qed.
imports: GeoCoq.Tarski_dev.Ch14_order