proposition: Lemma mid_par_cong2 : forall A B A' B' M, A <> B' -> Midpoint M A A' -> Midpoint M B B' -> Cong A B' A' B /\ Par A B' A' B.
proof: Proof. intros. spliter. split. apply (l7_13 M); Midpoint. eapply (l12_17 _ _ _ _ M); Midpoint. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel