proposition: Lemma i63leb_false_ltb (x y : i63) : x <=? y = false <-> y <? x = true.
proof: Proof. rewrite i63le_leb_false_equiv. rewrite i63lt_ltb_true_equiv. apply i63neg_le_lt. Qed.
imports: Coq(RelationClasses ZArith Int63 Lia)