proposition: Lemma lt_mid2__lt13 : forall A M B A' M' B', Midpoint M A B -> Midpoint M' A' B' -> Lt A M A' M' -> Lt A B A' B'.
proof: Proof. intros A M B A' M' B' HM HM' [HLe HNcong]. split. apply le_mid2__le13 with M M'; trivial. intro. apply HNcong, cong_cong_half_1 with B B'; trivial. Qed.
imports: GeoCoq.Tarski_dev.Ch06_out_lines GeoCoq.Tarski_dev.Tactics.ColR