proposition: Lemma l7_20 : forall M A B, Col A M B -> Cong M A M B -> A=B \/ Midpoint M A B.
proof: Proof. unfold Col. intros. induction H. right. unfold Midpoint. split. assumption. Cong. induction H. assert (Cong A B B B) by (apply (l4_3 A B M B B M);Between;Cong). treat_equalities;auto. assert (Cong B A A A) by (apply (l4_3 B A M A A M);Cong;Between). treat_equalities;auto. Qed.
imports: GeoCoq.Tarski_dev.Ch06_out_lines GeoCoq.Tarski_dev.Tactics.ColR