proposition: Lemma lt_farray_not_eq : forall m1 m2 : farray, lt_farray m1 m2 -> ~ eq m1 m2.
proof: Proof. intros (m1,Hm1,Hd1); induction m1; intros (m2,Hm2,Hd2); destruct m2; unfold eq, lt; simpl; try destruct a as (x,e); try destruct p as (x',e'); try contradiction; auto. destruct (compare x x') as [Hlt|Heq|Hlt]; auto. intuition. inversion_clear Hm1; inversion_clear Hm2. specialize (nodefault_tail Hd2). specialize (nodefault_tail Hd1). intros. subst. apply (IHm1 H0 H6 (Build_farray H4 H7)); intuition. unfold lt_farray in *. simpl in H. case (compare x' x') in *. apply lt_not_eq in l. now contradict l. destruct H. apply lt_not_eq in H. now contradict H. destruct H. auto. apply lt_not_eq in l. now contradict l. Qed.
imports: Bool OrderedType SMT_classes ProofIrrelevance