proposition: Lemma opp_same_square : forall O E E' A B A2, Opp O E E' A B -> Prod O E E' A A A2 -> Prod O E E' B B A2.
proof: Proof. intros. assert(~Col O E E'). unfold Prod in H0. spliter. unfold Ar2 in H0. tauto. assert(exists ME : Tpoint, Opp O E E' E ME). apply(opp_exists O E E' H1 E); Col; assert(HH:= opp_prod O E E'). ex_and H2 ME. assert(HH:= opp_prod O E E' ME A B H3 H). assert(Prod O E E' B ME A). apply(opp_prod O E E' ME B A H3). apply opp_comm; auto. assert(Prod O E E' ME B A). apply prod_comm; auto. assert(HP:=(prod_assoc O E E' A ME B B A A2 HH H4)). destruct HP. apply H5. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch16_coordinates