1 files changed, 14 insertions, 0 deletions
diff --git a/src/Galois/GaloisTheory.v b/src/Galois/GaloisTheory.v
index 8fa1b4113..ae8b290ad 100644
--- a/src/Galois/GaloisTheory.v
+++ b/src/Galois/GaloisTheory.v
@@ -180,6 +180,20 @@ Module GaloisTheory (M: Modulus).
     abstract (demod; trivial).
   Defined.
 
+  Lemma inject_distr_add : forall (m n : Z),
+      inject (m + n) = inject m + inject n.
+  Admitted.
+
+  Lemma inject_distr_mul : forall (m n : Z),
+      inject (m * n) = inject m * inject n.
+  Admitted.
+
+  Lemma inject_eq : forall (x : GF), inject x = x.
+  Admitted.
+
+  Lemma inject_mod_eq : forall x, inject x = inject (x mod modulus).
+  Admitted.
+
   Definition GFquotrem(a b: GF): GF * GF :=
     match (Z.quotrem a b) with
     | (q, r) => (inject q, inject r)