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