proposition: Lemma null_anga_null_anga' : forall a, Q_CongA_Null_Acute a <-> is_null_anga' a.
proof: Proof. intro. split. intro. unfold Q_CongA_Null_Acute in H. unfold is_null_anga'. spliter. split. auto. anga_instance a A B C. assert(HH:= H0 A B C H1). exists A. exists B. exists C. split; auto. intro. unfold is_null_anga' in H. unfold Q_CongA_Null_Acute. spliter. ex_and H0 A. ex_and H1 B. ex_and H0 C. split; auto. intros. assert(CongA A B C A0 B0 C0). apply (anga_conga a); auto. apply (l11_21_a A B C); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_2_length Setoid