proposition: Lemma leb_ltb_eqb : forall x y, ((x <=? y) = (x <? y) || (x =? y)).
proof: Proof. intros. apply eq_true_iff_eq. rewrite leb_spec, orb_true_iff, ltb_spec, eqb_spec, <- to_Z_eq;lia. Qed.
imports: Bool List PArray Int63 Ring63 ZArith Psatz