proposition: Lemma flat_ang : forall A B C A' B' C' a1 a2, Bet A B C -> Bet A' B' C' -> Ang A B C a1 -> Ang A' B' C' a2 -> EqA a1 a2.
proof: Proof. intros. eapply (all_eqa A B C). apply H1. eapply (is_ang_conga_is_ang A' B' C'). apply H2. apply is_ang_distinct in H1. apply is_ang_distinct in H2. spliter. eapply conga_line; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_2_length