proposition: Lemma square_increase : forall O E E' A B A2 B2, Ar2 O E E' A B A -> Ps O E A -> Ps O E B -> LeP O E E' A B -> Prod O E E' A A A2 -> Prod O E E' B B B2 -> LeP O E E' A2 B2.
proof: Proof. intros. unfold LeP in H2. induction H2. apply (square_increase_strict O E E' A B A2 B2) in H2; auto. apply ltp_to_lep in H2; auto. subst B. assert(A2 = B2). { apply (prod_uniqueness O E E' A A); auto. } subst B2. unfold LeP. right; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch14_order