proposition: Lemma mult_lt_compat_l'' : forall (p m k n : nat), lt 0 p -> lt n m -> lt k p -> lt ((p * n) + k) (p * m).
proof: Proof. induction p; intros; try omega. simpl. inversion H; subst; simpl. inversion H1; subst; omega. destruct k; simpl. - rewrite <- plus_n_O. eapply (mult_lt_compat_l n m (S p)); auto. - assert (lt (p * n + k) (p * m)) by (apply IHp; try omega). omega. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Strings.String Coq.Arith.Mult Coq.Vectors.Vector Fiat.Common.SumType Fiat.Common.BoundedLookup Fiat.Common.ilist Fiat.Common.DecideableEnsembles Fiat.Common.IterateBoundedIndex Fiat.Common.Tactics.CacheStringConstant Fiat.Computation Fiat.QueryStructure.Specification.Representation.Notations Fiat.QueryStructure.Specification.Representation.Heading Fiat.QueryStructure.Specification.Representation.Tuple Fiat.Narcissus.BinLib.Core Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Automation.Solver Fiat.Narcissus.Formats.WordOpt Fiat.Narcissus.Formats.NatOpt Fiat.Narcissus.Formats.StringOpt Fiat.Narcissus.Formats.EnumOpt Fiat.Narcissus.Formats.FixListOpt Fiat.Narcissus.Formats.SumTypeOpt Fiat.Narcissus.Formats.DomainNameOpt Fiat.Narcissus.Examples.DNS.DNSPacket Bedrock.Word