proposition: Lemma ltListTrans : forall m x y z, length x = (S m) -> length y = (S m) -> length z = (S m) -> ltList x y -> ltList y z -> ltList x z.
proof: Proof. intro m; induction m; intros x y z lx ly lz Hxy Hyz. assert (Hx := lengthOne x lx); destruct Hx as [hdx Hx]. assert (Hy := lengthOne y ly); destruct Hy as [hdy Hy]. assert (Hz := lengthOne z lz); destruct Hz as [hdz Hz]. subst; simpl in *. assert (H : Pos.ltb hdx hdz = true). rewrite Pos.ltb_lt. transitivity hdy. rewrite <- Pos.ltb_lt. induction (Pos.ltb hdx hdy); intuition. induction (Pos.ltb hdy hdx); intuition. rewrite <- Pos.ltb_lt. induction (Pos.ltb hdy hdz); intuition. induction (Pos.ltb hdz hdy); intuition. rewrite H; trivial. assert (Hx := lengthAtLeastOne x (S m) lx); destruct Hx as [hdx [tlx Hx]]. assert (Hy := lengthAtLeastOne y (S m) ly); destruct Hy as [hdy [tly Hy]]. assert (Hz := lengthAtLeastOne z (S m) lz); destruct Hz as [hdz [tlz Hz]]. subst; simpl in *. assert (HEqxy := Pos.compare_eq hdx hdy). assert (HEqyz := Pos.compare_eq hdy hdz). assert (HLtxy := Pos.compare_nge_iff hdx hdy). assert (HLtyz := Pos.compare_nge_iff hdy hdz). assert (HGtxy := Pos.compare_gt_iff hdx hdy). assert (HGtyz := Pos.compare_gt_iff hdy hdz). induction (Pos.compare hdx hdy); induction (Pos.compare hdy hdz). assert (H : Eq = Eq) by reflexivity. apply HEqxy in H; clear HEqxy; clear HLtxy; clear HGtxy. assert (H' : Eq = Eq) by reflexivity. apply HEqyz in H'; clear HEqyz; clear HLtyz; clear HGtyz. subst. assert (H := Pos.ltb_irrefl hdz). rewrite H in *; clear H. apply eq_add_S in lx. apply eq_add_S in ly. apply eq_add_S in lz. apply IHm with tly; assumption. assert (H : Eq = Eq) by reflexivity. apply HEqxy in H; clear HEqxy; clear HLtxy; clear HGtxy. assert (H' : Lt = Lt) by reflexivity. apply HLtyz in H'; clear HEqyz; clear HLtyz; clear HGtyz. subst. rewrite <- Pos.lt_nle in H'. rewrite <- Pos.ltb_lt in H'. rewrite H' in *. trivial. assert (H : Eq = Eq) by reflexivity. apply HEqxy in H; clear HEqxy; clear HLtxy; clear HGtxy. assert (H' : Gt = Gt) by reflexivity. apply HGtyz in H'; clear HEqyz; clear HLtyz; clear HGtyz. subst. rewrite <- Pos.ltb_lt in H'. rewrite H' in *. trivial. assert (H : Lt = Lt) by reflexivity. apply HLtxy in H; clear HEqxy; clear HLtxy; clear HGtxy. assert (H' : Eq = Eq) by reflexivity. apply HEqyz in H'; clear HEqyz; clear HLtyz; clear HGtyz. subst. rewrite <- Pos.lt_nle in H. rewrite <- Pos.ltb_lt in H. rewrite H in *. trivial. assert (H : Lt = Lt) by reflexivity. apply HLtxy in H; clear HEqxy; clear HLtxy; clear HGtxy. assert (H' : Lt = Lt) by reflexivity. apply HLtyz in H'; clear HEqyz; clear HLtyz; clear HGtyz. rewrite <- Pos.lt_nle in H. rewrite <- Pos.lt_nle in H'. assert (H'' : Pos.lt hdx hdz) by (transitivity hdy; assumption). rewrite <- Pos.ltb_lt in H''. rewrite H''. trivial. clear HEqxy; clear HLtxy; clear HGtxy. assert (H : Gt = Gt) by reflexivity. apply HGtyz in H; clear HEqyz; clear HLtyz; clear HGtyz. rewrite <- Pos.ltb_lt in H. rewrite H in *. rewrite Pos.ltb_lt in H. rewrite Pos.lt_nle in H. assert (H' : Pos.ltb hdy hdz = false). rewrite Pos.ltb_nlt. intro H'. apply H. apply Pos.lt_eq_cases. left; assumption. rewrite H' in *. intuition. clear HEqyz; clear HLtyz; clear HGtyz. assert (H : Gt = Gt) by reflexivity. apply HGtxy in H; clear HEqxy; clear HLtxy; clear HGtxy. rewrite <- Pos.ltb_lt in H. rewrite H in *. rewrite Pos.ltb_lt in H. rewrite Pos.lt_nle in H. assert (H' : Pos.ltb hdx hdy = false). rewrite Pos.ltb_nlt. intro H'. apply H. apply Pos.lt_eq_cases. left; assumption. rewrite H' in *. intuition. clear HEqyz; clear HLtyz; clear HGtyz. assert (H : Gt = Gt) by reflexivity. apply HGtxy in H; clear HEqxy; clear HLtxy; clear HGtxy. rewrite <- Pos.ltb_lt in H. rewrite H in *. rewrite Pos.ltb_lt in H. rewrite Pos.lt_nle in H. assert (H' : Pos.ltb hdx hdy = false). rewrite Pos.ltb_nlt. intro H'. apply H. apply Pos.lt_eq_cases. left; assumption. rewrite H' in *. intuition. clear HEqyz; clear HLtyz; clear HGtyz. assert (H : Gt = Gt) by reflexivity. apply HGtxy in H; clear HEqxy; clear HLtxy; clear HGtxy. rewrite <- Pos.ltb_lt in H. rewrite H in *. rewrite Pos.ltb_lt in H. rewrite Pos.lt_nle in H. assert (H' : Pos.ltb hdx hdy = false). rewrite Pos.ltb_nlt. intro H'. apply H. apply Pos.lt_eq_cases. left; assumption. rewrite H' in *. intuition. Qed.
imports: MSets Arith NArith Notations Sorting Coq.Program.Equality GeoCoq.Tactics.Coinc.tactics_axioms