proposition: Lemma l7_20_bis : forall M A B, A<>B -> Col A M B -> Cong M A M B -> Midpoint M A B.
proof: Proof. intros. induction (l7_20 M A B H0 H1);intuition. Qed.
imports: GeoCoq.Tarski_dev.Ch06_out_lines GeoCoq.Tarski_dev.Tactics.ColR