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