proposition: Lemma lea_obtuse_obtuse : forall A B C D E F, Obtuse D E F -> LeA D E F A B C -> Obtuse A B C.
proof: Proof. intros. ex_and H A'. ex_and H1 B'. ex_and H C'. exists A', B', C'. split. assumption. assert(HH1:=H1). unfold LtA in H1. spliter. split. eapply lea_trans. apply H1. assumption. intro. assert(LtA D E F A' B' C'). eapply conga_preserves_lta. apply conga_refl. unfold LeA in H0. ex_and H0 X. unfold CongA in H4. spliter. assumption. apply lea_comm in H0. unfold LeA in H0. ex_and H0 X. unfold CongA in H4. spliter. assumption. apply conga_sym. apply H3. split. assumption. intro. apply H2. eapply conga_trans. apply H3. apply conga_sym. assumption. apply (not_and_lta A' B' C' D E F). split; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2