proposition: Lemma pred_lt_beq {x} : negb (Nat.eqb x 0) = true -> pred x < x.
proof: Proof. destruct x; simpl; try congruence; try omega. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Lists.List Coq.ZArith.ZArith Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.BaseTypes Fiat.Parsers.GenericBaseTypes Fiat.Common.Wf