Lemma boolnegtrueimplfalse ( v : bool ) ( p : neg ( v = true ) ) : v = false. Proof. intros. destruct v. - apply fromempty. apply p; auto. - auto. Defined.
Require Import UniMath.Foundations.PartA. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.Algebra.Domains_and_Fields. Require Import UniMath.NumberSystems.Integers. Require Import UniMath.Algebra.Monoids.