proposition: Lemma IS_seq : IS (red_mod E R) seq.
proof: Proof. intro n; pattern n; apply lt_wf_ind; clear n; intros. unfold seq at -2 . destruct (eucl_dev k h0 n); simpl. destruct (le_gt_dec (k-1) r). assert (r = k-1). lia. assert (S n = (S q)*k + 0). rewrite Nat.mul_succ_l. lia. rewrite H1. unfold seq. destruct (eucl_dev k h0 (S q * k + 0)). destruct (eucl_div_unique h0 g1 e0). rewrite <- H3, <- H2. simpl. rewrite <- iter_com. apply red_iter. apply red_mod_fill. rewrite H0. fold last_string. cut (red_mod E R (g t) (g (nth 0))). intro. destruct H4. exists x. intuition. apply rt_trans with (g t). apply red_last_string_g. hyp. apply red_mod_fill. unfold nth. change (red_mod E R (List.nth 0 (t :: us) default) (List.nth 1 (t :: us) default)). apply red_mod_nth. apply (mod_rewrites_correct h1). hyp. assert (S n = q*k + S r). lia. rewrite H0. unfold seq. destruct (eucl_dev k h0 (q * k + S r)). assert (k>S r). lia. destruct (eucl_div_unique H1 g2 e0). rewrite <- H3, <- H2. apply red_iter. apply red_mod_fill. apply FS_red_mod'. lia. Qed.
imports: Coq(Euclid Wf_nat) CoLoR(Srs LogicUtil SLoop ListUtil NatUtil RelUtil)