proposition: Lemma slt_list_big_endian_not_eq : forall x y, slt_list_big_endian x y = true -> x <> y.
proof: Proof. intros x. induction x. simpl. easy. intros y. case y. simpl. case x; easy. intros b l. simpl. specialize (IHx l). case x in *. simpl. case l in *. case a; case b; simpl; easy. easy. rewrite !orb_true_iff, !andb_true_iff. intro. destruct H. destruct H. apply ult_list_big_endian_not_eq in H0. apply Bool.eqb_prop in H. rewrite H in *. unfold not in *. intros. apply H0. now inversion H1. destruct H. apply negb_true_iff in H0. subst. easy. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance