proposition: Lemma le_mid2__le13 : forall A M B A' M' B', Midpoint M A B -> Midpoint M' A' B' -> Le A M A' M' -> Le A B A' B'.
proof: Proof. intros A M B A' M' B' HM HM' Hle. destruct HM. destruct HM'. apply (bet2_le2__le1346 _ M _ _ M'); auto. apply (l5_6 A M A' M'); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch06_out_lines GeoCoq.Tarski_dev.Tactics.ColR