lemma leb_eqb : ∀n,m. orb (eqb n m) (leb (S n) m) = leb n m.
intros (n m); apply bool_to_eq; split; intros (H);
-[1:cases (b2pT ? ? (orbP ? ?) H); [2: autobatch]
+[1:cases (b2pT ? ? (orbP ? ?) H); [2: autobatch type]
rewrite > (eqb_true_to_eq ? ? H1); autobatch
|2:cases (b2pT ? ? (lebP ? ?) H);
[ elim n; [reflexivity|assumption]