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