proposition: Lemma nlt_neq_gt: forall x y, length x = length y -> ult_list x y = false -> beq_list x y = false -> ult_list y x = true.
proof: Proof. intros. unfold ult_list in *. apply nlt_be_neq_gt. now rewrite !rev_length. easy. now apply rev_neq in H1. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance