proposition: Lemma is_anga_conga : forall A B C A' B' C' a, Ang_Acute A B C a -> Ang_Acute A' B' C' a -> CongA A B C A' B' C'.
proof: Proof. intros. unfold Ang_Acute in *. spliter. apply (anga_conga a); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_2_length Setoid