(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/decidable_kit/decidable/".
-
(* classical connectives for decidable properties *)
include "decidable_kit/streicher.ma".
[1: intros; cases (b2pT ? ? (orbP ? ?) H); [1: apply ltbW; assumption]
rewrite > (eqb_true_to_eq ? ? H1); simplify;
rewrite > leb_refl; reflexivity
-|2: generalize in match m; clear m; elim n 0;
+|2: elim n in m ⊢ % 0;
[1: simplify; intros; cases n1; reflexivity;
|2: intros 1 (m); elim m 0;
[1: intros; apply (p2bT ? ? (orbP ? ?));