proposition: Lemma mult_lt_compat_l' : forall (m n p : nat), lt 0 p -> lt (p * n) (p * m) -> lt n m.
proof: Proof. induction m; simpl; intros; try omega. rewrite (mult_comm p 0) in H0; simpl in *; try omega. destruct p; try (exfalso; auto with arith; omega). inversion H0. rewrite (mult_comm p (S m)) in H0. simpl in H0. destruct n; try omega. rewrite (mult_comm p (S n)) in H0; simpl in H0. apply plus_lt_reg_l in H0. rewrite <- NPeano.Nat.succ_lt_mono. eapply (IHm n p); try eassumption; try omega. rewrite mult_comm. rewrite (mult_comm p m); auto. 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