proposition: Lemma not_conga_not_ang : forall A B C A' B' C' a , Q_CongA a -> ~(CongA A B C A' B' C') -> a A B C -> ~(a A' B' C').
proof: Proof. intros. intro. assert(HH:=ang_conga a A B C A' B' C' H H1 H2). contradiction. Qed.
imports: GeoCoq.Tarski_dev.Ch13_2_length