proposition: Lemma ang_cong_ang : forall a A B C A' B' C', Q_CongA a -> a A B C -> CongA A B C A' B' C' -> a A' B' C'.
proof: Proof. intros. assert(Ang A B C a). unfold Ang. split; auto. assert(Ang A' B' C' a). apply (is_ang_conga_is_ang A B C); auto. unfold Ang in H3. tauto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_2_length Setoid