proposition: Lemma mid_par_cong1 : 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. split. eapply (l7_13 M); Midpoint. apply (l12_17 _ _ _ _ M); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel