proposition: Lemma is_null_anga_dec : forall a, Q_CongA_Acute a -> Q_CongA_Null_Acute a \/ ~ Q_CongA_Null_Acute a.
proof: Proof. intros a H. assert (H' := H). unfold Q_CongA_Acute in H. destruct H as [A [B [C [Hacute HConga]]]]. elim (out_dec B A C); intro Hout. left. unfold Q_CongA_Null_Acute. split; auto. intros. apply (l11_21_a A B C); auto. apply HConga. assumption. right. unfold Q_CongA_Null_Acute. intro H. destruct H as [Hclear H]; clear Hclear. apply Hout. apply H. apply HConga. apply acute_distincts in Hacute. spliter. apply conga_refl; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_3_angles Morphisms