proposition: Lemma anga_conga : forall a A B C A' B' C', Q_CongA_Acute a -> a A B C -> a A' B' C' -> CongA A B C A' B' C'.
proof: Proof. intros. apply (ang_conga a); auto. apply anga_is_ang. auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_2_length Setoid