fact: Definition isconnected_pred_add n m A `{H : IsConnected (n +2+ m) A} : IsConnected m A.
imports: Basics Types Extensions Factorization Modalities.Modality Modalities.Descent Truncations.Core Truncations.SeparatedTrunc