proposition: Lemma anga_not_flat : forall a, Q_CongA_Acute a -> Q_CongA_nFlat a.
proof: Proof. intros. unfold Q_CongA_nFlat. split. apply anga_is_ang in H. auto. intros. assert(HH:= anga_acute a A B C H H0). unfold Q_CongA_Acute in H. ex_and H A0. ex_and H1 B0. ex_and H C0. assert(HP:= H1 A B C). apply acute_not_bet. auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_2_length Setoid