proposition: Lemma le_le_S_eq : forall (n m: nat), (n <= m)%nat -> (S n <= m)%nat \/ n = m.
proof: Proof. Proof le_lt_or_eq. Lemma diseq_neg_eq: forall (la lb: list bool), List_diseqb la lb = true -> negb (RAWBITVECTOR_LIST.beq_list la lb) = true. Proof. intro la. induction la. - intros. simpl in H. case lb in *. now contradict H. now simpl. - intros. simpl in *. case lb in *. easy. case_eq (Bool.eqb a false). intros. rewrite H0 in H. case_eq (Bool.eqb b false). intros. rewrite H1 in H. case a in *. now contradict H0. case b in *. now contradict H1. simpl. apply IHla. easy. case a in *. now contradict H0. case b in *. intros. now simpl. intros. simpl. apply IHla. simpl in H. easy. intros. rewrite H0 in H. case_eq (Bool.eqb b true ). intros. case a in *. case b in *. simpl. apply IHla. simpl in H. easy. now simpl. now contradict H0. intros. case a in *. case b in *. simpl in *. now contradict H1. now simpl in *. case b in *. now simpl in *. simpl in *. now contradict H. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance