proposition: Lemma ult_list_not_eq : forall x y, ult_list x y = true -> x <> y.
proof: Proof. unfold ult_list. unfold not. intros. apply ult_list_big_endian_not_eq in H. subst. auto. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance