|2:cases (b2pT ? ? (lebP ? ?) H);
[ elim n; [reflexivity|assumption]
| simplify; rewrite > (p2bT ? ? (lebP ? ?) H1); rewrite > orbC ]
|2:cases (b2pT ? ? (lebP ? ?) H);
[ elim n; [reflexivity|assumption]
| simplify; rewrite > (p2bT ? ? (lebP ? ?) H1); rewrite > orbC ]