proposition: Lemma not_conga_is_ang : forall A B C A' B' C' a , ~(CongA A B C A' B' C') -> Ang A B C a -> ~(a A' B' C').
proof: Proof. intros. unfold Ang in H0. spliter. intro. apply H. apply (ang_conga a); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_2_length