proposition: Lemma midpoint_par_strict : forall A B A' B' M, ~ Col A B B' -> Midpoint M A A' -> Midpoint M B B' -> Par_strict A B A' B'.
proof: Proof. intros. assert (A <> B). apply not_col_distincts in H; spliter; assumption. assert(Par A B A' B'). eapply (midpoint_par A B A' B' M); assumption. induction H3. assumption. spliter. apply False_ind. assert(HH:=midpoint_col B' A' B A M). assert(B <> A /\ Col B' B A /\ Col A' B A). apply HH. auto. apply l7_2. assumption. apply l7_2. assumption. Col. spliter. apply H. Col. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec