proposition: Lemma square_increase_strict : forall O E E' A B A2 B2, Ar2 O E E' A B A -> Ps O E A -> Ps O E B -> LtP O E E' A B -> Prod O E E' A A A2 -> Prod O E E' B B B2 -> LtP O E E' A2 B2.
proof: Proof. intros. assert(HA2 : Col O E A2). { apply (prod_col O E E' A A); auto. unfold Ar2 in *. tauto. } assert(HB2: Col O E B2). { apply (prod_col O E E' B B); auto. unfold Ar2 in *. tauto. } unfold Ar2 in H. spliter. assert(HD:=diff_exists O E E' B A H H6 H7). ex_and HD BmA. assert(HS:=sum_exists O E E' H B A H6 H7). ex_and HS BpA. assert(HD:=diff_exists O E E' B2 A2 H HB2 HA2). ex_and HD B2mA2. assert(Col O E BpA). { apply sum_ar2 in H9. unfold Ar2 in H9. tauto. } assert(Col O E BmA). { apply diff_ar2 in H8. unfold Ar2 in H8. tauto. } assert(Col O E B2mA2). { apply diff_ar2 in H10. unfold Ar2 in H10. tauto. } assert(HP:= prod_exists O E E' H BpA BmA H11 H12). ex_and HP F. assert(HC:= diff_of_squares O E E' B A B2 A2 B2mA2 BpA BmA F H4 H3 H10 H9 H8 H14). subst F. unfold LtP. exists B2mA2. split; auto. apply (prod_pos_pos O E E' BpA BmA); auto. apply (sum_pos_pos O E E' B A); auto. apply (lt_diff_ps O E E' B A); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch14_order