proposition: Lemma leb_ltb_trans : forall x y z, x <=? y = true -> y <? z = true -> x <? z = true.
proof: Proof. intros x y z;rewrite leb_spec, !ltb_spec;apply Z.le_lt_trans. Qed.
imports: Bool List PArray Int63 Ring63 ZArith Psatz