proposition: Lemma square_pos : forall O E E' A A2, O <> A -> Prod O E E' A A A2 -> Ps O E A2.
proof: Proof. intros O E E' A A2 HDiff HA2. assert (HNC : ~ Col O E E') by (unfold Prod, Ar2 in *; spliter; Col). assert (HColA : Col O E A) by (unfold Prod, Ar2 in *; spliter; Col). destruct (opp_exists O E E' HNC A) as [MA HMA]; Col. assert (HElim := HMA); apply pos_null_neg in HElim. elim HElim; clear HElim; intro HElim; [apply prod_pos_pos with E' A A; auto|]. elim HElim; clear HElim; intro HPs; [intuition|apply prod_pos_pos with E' MA MA; auto]. destruct (opp_exists O E E' HNC E) as [ME HME]; Col. apply prod_assoc1 with A ME A; auto; [|apply prod_comm]; apply opp_prod; auto. apply opp_comm; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch14_prod