proposition: Lemma symmetry_preserves_conga : forall A B C A' B' C' M, A <> B -> C <> B -> Midpoint M A A' -> Midpoint M B B' -> Midpoint M C C' -> CongA A B C A' B' C'.
proof: Proof. intros. assert(Cong A B A' B'). apply (l7_13 M); Midpoint. assert(Cong B C B' C'). apply (l7_13 M); Midpoint. assert(Cong A C A' C'). apply (l7_13 M); Midpoint. apply cong3_conga; auto. repeat split; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2