proposition: Lemma FS_red_mod' : forall i, i < k - 1 -> red_mod E R (nth i) (nth (S i)).
proof: Proof. intros. unfold nth. change (red_mod E R (List.nth (S i) (t :: us) default) (List.nth (S (S i)) (t :: us) default)). apply red_mod_nth. eapply mod_rewrites_correct. apply h1. unfold k in *. lia. Qed.
imports: Coq(Euclid Wf_nat) CoLoR(Srs LogicUtil SLoop ListUtil NatUtil RelUtil)