proposition: Lemma not_cong_is_anga1 : forall A B C A' B' C' a , ~ CongA A B C A' B' C' -> Ang_Acute A B C a -> ~ Ang_Acute A' B' C' a.
proof: Proof. intros. intro. unfold Ang_Acute in *. spliter. apply H. apply (anga_conga a); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_2_length Setoid