diff --git a/FilteredRing/graded.lean b/FilteredRing/graded.lean
index 9d94970..1e22c5f 100644
--- a/FilteredRing/graded.lean
+++ b/FilteredRing/graded.lean
@@ -7,7 +7,9 @@ variable {ι : Type v} [OrderedAddCommMonoid ι] [DecidableEq ι] [PredOrder ι]
 
 variable (F : ι → AddSubgroup R) [FilteredRing F]
 
+instance {i : ι}: F (PredOrder.pred i) ≤ F i :=
+  FilteredRing.mono (PredOrder.pred i) (PredOrder.pred_le i)
 
-def gradedMap (F : ι → AddSubgroup R) [FilteredRing F] : ι → AddSubgroup R := sorry
+def gradedMap {i : ι} : Module R ((F i) ⧸ (F (PredOrder.pred i)).addSubgroupOf (F i)) := sorry
 
-instance : GradedRing (gradedMap F) := sorry
+-- instance : GradedRing (gradedMap F) := sorry