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