proposition: Lemma l11_51 : forall A B C A' B' C', A <> B -> A <> C -> B <> C -> Cong A B A' B' -> Cong A C A' C' -> Cong B C B' C' -> CongA B A C B' A' C' /\ CongA A B C A' B' C' /\ CongA B C A B' C' A'.
proof: Proof. intros. assert(Cong_3 B A C B' A' C' /\ Cong_3 A B C A' B' C' /\ Cong_3 B C A B' C' A'). repeat split; Cong. spliter. split; [|split]; apply cong3_conga; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2