proposition: Lemma bv_ult_not_eqP: forall n (a b: bitvector n), bv_ultP a b -> a <> b.
proof: Proof. unfold bv_ultP, bv_ult. intros n a b H. apply M.bv_ult_not_eqP in H. unfold not in *; intros. apply H. apply M.bv_eq_reflect. rewrite H0. apply M.bv_eq_refl. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance