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