proposition: Lemma slt_list_not_eqP : forall x y, slt_listP x y -> x <> y.
proof: Proof. unfold slt_listP. unfold not. intros. unfold slt_list in H. case_eq (slt_list_big_endian (List.rev x) (List.rev y)); intros. apply slt_list_big_endian_not_eq in H1. subst. now contradict H1. now rewrite H1 in H. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance