Require Import ZArith.

Module Type Zahl.
  Parameter Zahl : Type.
  Parameter plus : Zahl -> Zahl -> Zahl.
  Parameter zerop : Zahl -> bool.
End Zahl.

Module ZDirect <: Zahl.
  Definition Zahl := Z.
  Definition plus := Zplus.
  Definition zerop := fun z => if Z_zerop z then true else false.
End ZDirect.

Module ZQuotient <: Zahl.
  Definition Zahl := (nat * nat)%type.
  Definition plus x y :=
    match x, y with (a,b),(c,d) =>
      (a + c,b + d)
    end.
  Definition zerop x :=
    match x with (a,b) =>
      if eq_nat_dec a b
        then true
        else false
    end.
End ZQuotient.

Module MyModule (Integer : Zahl).
  Import Integer.
  Definition funky (a : Zahl) :=
    if zerop (plus a a)
      then a
      else plus a (plus a a).
End MyModule.

Module Z1 := MyModule ZDirect.
Module Z2 := MyModule ZQuotient.

Check (Z1.funky).


Axiom R : (nat*nat)%type -> (nat*nat)%type -> Prop.
Axiom ZD_to_ZQ : Z -> (nat*nat)%type.
Axiom ZQ_to_ZD : (nat*nat)%type -> Z.
Axiom isomorphism1 : forall z,
  ZQ_to_ZD (ZD_to_ZQ z) = z.
Axiom isomorphism2 : forall z,
  R (ZD_to_ZQ (ZQ_to_ZD z)) z.
Axiom isomorphism_respectful : forall z z', R z z' -> ZQ_to_ZD z = ZQ_to_ZD z'.

Theorem funky_respectful : forall a b : (nat*nat)%type, R a b -> R (Z2.funky a) (Z2.funky b).