proposition: 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: 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.
imports: UniMath.Tactics.EnsureStructuredProofs UniMath.Foundations.PartA UniMath.Foundations.Propositions UniMath.Foundations.NaturalNumbers UniMath.Algebra.RigsAndRings UniMath.Algebra.Domains_and_Fields UniMath.NumberSystems.Integers UniMath.Algebra.Monoids