proposition: Lemma i63ltb_false_leb (x y : i63) : x <? y = false <-> y <=? x = true.
proof: Proof. rewrite i63lt_ltb_false_equiv. rewrite i63le_leb_true_equiv. apply i63neg_lt_le. Qed.
imports: Coq(RelationClasses ZArith Int63 Lia)