proposition: Lemma null_ang : forall A B C D a1 a2, Ang A B A a1 -> Ang C D C a2 -> EqA a1 a2.
proof: Proof. intros. eapply (all_eqa A B A). apply H. eapply (is_ang_conga_is_ang C D C). auto. eapply l11_21_b. apply out_trivial. apply is_ang_distinct in H0. tauto. apply out_trivial. apply is_ang_distinct in H. tauto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_2_length