proposition: Lemma isaprop_dec_with_negProp {P : hProp} (Q : negProp P) : isaprop (P ⨿ Q).
proof: Proof. apply isapropcoprod. - apply propproperty. - apply propproperty. - intros p q; revert p. apply (negProp_to_neg q). Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Combinatorics.Maybe UniMath.Combinatorics.StandardFiniteSets UniMath.Algebra.Domains_and_Fields UniMath.Algebra.RigsAndRings