[1: intros; cases (b2pT ? ? (orbP ? ?) H); [1: apply ltbW; assumption]
rewrite > (eqb_true_to_eq ? ? H1); simplify;
rewrite > leb_refl; reflexivity
[1: intros; cases (b2pT ? ? (orbP ? ?) H); [1: apply ltbW; assumption]
rewrite > (eqb_true_to_eq ? ? H1); simplify;
rewrite > leb_refl; reflexivity