proposition: Lemma lt_farray_trans : forall m1 m2 m3 : farray, lt_farray m1 m2 -> lt_farray m2 m3 -> lt_farray m1 m3.
proof: Proof. intros (m1,Hm1,d1,Hd1); induction m1; intros (m2,Hm2,d2,Hd2); destruct m2; intros (m3,Hm3,d3,Hd3); destruct m3; unfold lt_farray; simpl; try destruct a as (x,e); try destruct p as (x',e'); try destruct p0 as (x'',e''); try contradiction; intuition; auto; try (left; apply (lt_trans d1 d2 d3); now auto); try (left; subst; now auto); try (right; subst; auto). split; auto. destruct (compare x x') as [Hlt|Heq|Hlt]; destruct (compare x' x'') as [Hlt'|Heq'|Hlt']; destruct (compare x x'') as [Hlt''|Heq''|Hlt'']; intros; subst; auto; try easy. apply (lt_trans x') in Hlt; apply lt_not_eq in Hlt. now contradict Hlt. auto. apply (lt_trans x') in Hlt; apply lt_not_eq in Hlt. now contradict Hlt. apply (lt_trans _ x'') ; auto. apply lt_not_eq in Hlt. now contradict Hlt. apply (lt_trans x'') in Hlt; apply lt_not_eq in Hlt. now contradict Hlt. auto. subst. apply lt_not_eq in Hlt'. now contradict Hlt'. apply (lt_trans x'') in Hlt'; apply lt_not_eq in Hlt'. now contradict Hlt'. auto. destruct H2, H3. left; apply lt_trans with e'; auto. left. destruct H0. subst; auto. left. destruct H. subst; auto. right. destruct H, H0. subst; split; auto. inversion_clear Hm1; inversion_clear Hm2; inversion_clear Hm3. apply nodefault_tail in Hd1. apply nodefault_tail in Hd2. apply nodefault_tail in Hd3. specialize (IHm1 H Hd1 (Build_slist H3 Hd2) (Build_slist H5 Hd3)). unfold lt_farray in IHm1. simpl in IHm1. destruct IHm1; auto. apply lt_not_eq in H7. now contradict H7. destruct H7; auto. apply lt_not_eq in Hlt''. now contradict Hlt''. Qed.
imports: Bool OrderedType SMT_classes ProofIrrelevance