proposition: Lemma nlt_be_neq_gt: forall x y, length x = length y -> ult_list_big_endian x y = false -> beq_list x y = false -> ult_list_big_endian y x = true.
proof: Proof. intro x. induction x as [ | x xs IHxs ]. - intros. simpl in *. case y in *; now contradict H. - intros. simpl in H1. case_eq y; intros. rewrite H2 in H. now contradict H. simpl. case_eq l. intros. case_eq xs. intros. rewrite H2 in H1. rewrite H4 in H0, H. simpl in H0, H. rewrite H2, H3 in H0, H. rewrite H4, H3 in H1. simpl in H1. rewrite andb_true_r in H1. case b in *; case x in *; easy. intros. rewrite H4, H2, H3 in H. now contradict H. intros. rewrite H2, H3 in H0, H1. simpl in H0. case_eq xs. intros. rewrite H4, H2, H3 in H. now contradict H. intros. rewrite H4 in H0. rewrite <- H3, <- H4. rewrite <- H3, <- H4 in H0. rewrite <- H3 in H1. rewrite orb_false_iff in H0. destruct H0. case_eq (Bool.eqb x b); intros. rewrite H6 in H0, H1. rewrite andb_true_l in H0, H1. assert (Bool.eqb b x = true). { case b in *; case x in *; easy. } rewrite H7. rewrite andb_true_l. rewrite orb_true_iff. left. apply IHxs. rewrite H2 in H. now inversion H. easy. easy. assert (Bool.eqb b x = false). { case b in *; case x in *; easy. } rewrite H7. rewrite orb_false_l. case x in *. case b in *. now contradict H6. now easy. case b in *. now contradict H5. now contradict H6. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance