proposition: Lemma le_mid2__le12 : forall A M B A' M' B', Midpoint M A B -> Midpoint M' A' B' -> Le A B A' B' -> Le A M A' M'.
proof: Proof. intros A M B A' M' B' HM HM' Hle. elim(le_cases A M A' M'); auto. intro. assert(Le A' B' A B) by (apply (le_mid2__le13 _ M' _ _ M); auto). apply cong__le. apply (cong_cong_half_1 _ _ B _ _ B'); auto. apply le_anti_symmetry; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch06_out_lines GeoCoq.Tarski_dev.Tactics.ColR