proposition: Lemma pathssminus ( n m : nat ) ( p : natlth m ( S n ) ) : S ( sub n m ) = sub ( S n ) m.
proof: Proof. revert m p. induction n. - intros m p. destruct m. + auto. + apply fromempty. apply nopathstruetofalse. apply pathsinv0. assumption. - intros m p. destruct m. + auto. + apply IHn. apply p. 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