proposition: Lemma bv_slt_not_eqP : forall x y, bv_sltP x y -> x <> y.
proof: Proof. intros x y. unfold bv_sltP. case_eq (size x =? size y)%N; intros. - now apply slt_list_not_eqP in H0. - now contradict H0. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance