Lemma natdoubleminus { n k l : nat } ( p : natleh k n ) ( q : natleh l k ) : sub n k = sub ( sub n l ) ( sub k l ). Proof. revert k l p q. induction n. - auto. - intros k l p q. destruct k. + destruct l. * auto. * apply fromempty. exact ( negnatlehsn0 l q ). + destruct l. * auto. * apply ( IHn k l ); assumption. 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.