proposition: Lemma is_anga_distinct : forall A B C a , Ang_Acute A B C a -> A <> B /\ C <> B.
proof: Proof. intros. apply (is_ang_distinct A B C a). apply is_anga_to_is_ang. auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_2_length Setoid