proposition: Lemma conga_obtuse__obtuse : forall A B C D E F, Obtuse A B C -> CongA A B C D E F -> Obtuse D E F.
proof: Proof. intros A B C D E F Hobtuse HConga. apply (lea_obtuse_obtuse _ _ _ A B C); auto. apply conga__lea; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2