proposition: Lemma l11_49 : forall A B C A' B' C', CongA A B C A' B' C' -> Cong B A B' A' -> Cong B C B' C' -> Cong A C A' C' /\ (A <> C -> CongA B A C B' A' C' /\ CongA B C A B' C' A').
proof: Proof. intros. assert(Cong A C A' C'). eapply cong2_conga_cong. apply H. apply cong_commutativity. assumption. assumption. split. assumption. intro. assert(A <> B /\ C <> B /\ A' <> B' /\ C' <> B'). unfold CongA in H. spliter. repeat split; assumption. spliter. split. apply l11_3_bis. exists B. exists C. exists B'. exists C'. split. apply out_trivial. auto. split. apply out_trivial. auto. split. apply out_trivial. auto. split. apply out_trivial. intro. subst C'. apply cong_identity in H2. contradiction. repeat split; assumption. apply l11_3_bis. exists B, A, B', A'. split. apply out_trivial. auto. split. apply out_trivial. auto. split. apply out_trivial. auto. split. apply out_trivial. intro. subst C'. apply cong_identity in H2. contradiction. repeat split. assumption. assumption. apply cong_commutativity. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2