(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/decidable_kit/decidable/".
-
(* classical connectives for decidable properties *)
include "decidable_kit/streicher.ma".
lemma andbPF : ∀a,b:bool. reflect (a = false ∨ b = false) (negb (andb a b)).
intros (a b); apply prove_reflect; cases a; cases b; simplify; intros (H);
-[1,2,3,4: rewrite > H; [1,2:right|3,4:left] reflexivity
+[1,2,3,4: try rewrite > H; [1,2:right|3,4:left] reflexivity
|5,6,7,8: unfold Not; intros (H1); [2,3,4: destruct H]; cases H1; destruct H2]
qed.
[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 ? ?));