proposition: Lemma cong2_conga_obtuse__cong_conga2 : forall A B C A' B' C', Obtuse A B C -> CongA A B C A' B' C' -> Cong A C A' C' -> Cong B C B' C' -> Cong B A B' A' /\ CongA B A C B' A' C' /\ CongA B C A B' C' A'.
proof: Proof. intros. apply (l11_52 A B C A' B' C'); auto. destruct (col_dec A B C). apply bet__le2313, col_obtuse__bet; assumption. assert_diffs; apply l11_46; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2