freescle porting, work in progress

[helm.git] / helm / software / matita / contribs / ng_assembly / num / bool_lemmas.ma

diff --git a/helm/software/matita/contribs/ng_assembly/num/bool_lemmas.ma b/helm/software/matita/contribs/ng_assembly/num/bool_lemmas.ma
index 25d855d3186f87218733f68bb7f89cd8957c6a74..3549148de644eb4e847b95d1953fe8ac6ac71fee 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/num/bool_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/bool_lemmas.ma
@@ -132,43 +132,34 @@ nlemma eq_to_eqbool : ∀b1,b2.b1 = b2 → eq_bool b1 b2 = true.
  ##]
 nqed.
 
-nlemma neqbool_to_neq : ∀b1,b2:bool.(eq_bool b1 b2 = false) → (b1 ≠ b2).
- #b1; #b2;
- ncases b1;
- ncases b2;
- nnormalize;
- ##[ ##1,4: #H; napply (bool_destruct … H)
- ##| ##*: #H; #H1; napply (bool_destruct … H1)
- ##]
-nqed.
-
-nlemma neq_to_neqbool : ∀b1,b2.b1 ≠ b2 → eq_bool b1 b2 = false.
+nlemma andb_true_true_l: ∀b1,b2.(b1 ⊗ b2) = true → b1 = true.
  #b1; #b2;
  ncases b1;
  ncases b2;
  nnormalize;
- ##[ ##1,4: #H; napply False_ind; napply (H (refl_eq …))
- ##| ##*: #H; napply refl_eq
+ ##[ ##1,2: #H; napply refl_eq
+ ##| ##*: #H; napply (bool_destruct … H)
  ##]
 nqed.
 
-nlemma andb_true_true_l: ∀b1,b2.(b1 ⊗ b2) = true → b1 = true.
+nlemma andb_true_true_r: ∀b1,b2.(b1 ⊗ b2) = true → b2 = true.
  #b1; #b2;
  ncases b1;
  ncases b2;
  nnormalize;
- ##[ ##1,2: #H; napply refl_eq
+ ##[ ##1,3: #H; napply refl_eq
  ##| ##*: #H; napply (bool_destruct … H)
  ##]
 nqed.
 
-nlemma andb_true_true_r: ∀b1,b2.(b1 ⊗ b2) = true → b2 = true.
+nlemma andb_false : ∀b1,b2.(b1 ⊗ b2) = false → (b1 = false) ∨ (b2 = false).
  #b1; #b2;
  ncases b1;
  ncases b2;
  nnormalize;
- ##[ ##1,3: #H; napply refl_eq
- ##| ##*: #H; napply (bool_destruct … H)
+ ##[ ##1: #H; napply (bool_destruct … H)
+ ##| ##2,4: #H; napply (or_intror … H)
+ ##| ##3: #H; napply (or_introl … H)
  ##]
 nqed.