proposition: Lemma ltb_ge: forall n m, Nat.ltb n m = false <-> n >= m.
proof: Proof. unfold Nat.ltb; intros. revert n. induction m; destruct n; simpl; intuition auto; try discriminate || lia. apply IHm in H; lia. apply IHm; lia. Qed.
imports: Coq(FunctionalExtensionality List Arith Lia) Chapar(Predefs KVStore)