proposition: Lemma inv_col : forall A B, inv O E E' A B -> Col O E B.
proof: Proof. intros A B H; elim (eq_dec_points A O); intro HNEq; [induction H; spliter;[subst; intuition|treat_equalities; Col]|]. try (subst;Col). elim H; clear H; intro H; [clear HNEq|spliter; subst; intuition]. destruct H as [IA [HNEq HIA]]; unfold Ar2 in *; spliter; Col. Qed.
imports: Description Ring Field Nsatz Rtauto GeoCoq.Tarski_dev.Ch16_coordinates GeoCoq.Tarski_dev.Ch15_pyth_rel GeoCoq.Tarski_dev.Annexes.midpoint_theorems