proposition: Lemma ang_distinct: forall a A B C, Q_CongA a -> a A B C -> A <> B /\ C <> B.
proof: Proof. intros. assert(Ang A B C a). split; auto. apply (is_ang_distinct _ _ _ a); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_2_length