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