proposition: Lemma lincombmodzlincombmod : forall (c x y : Z) (n : nat), LinCombMod c x y n -> ZLinCombMod c x y (Z_of_nat n).
proof: Proof. unfold LinCombMod, ZLinCombMod in |- *. intros. elim H. intros z Hz. exists z. elim Hz. intros b Hb. exists b. apply modzmod. assumption. Qed.
imports: ZArith Wf_nat lemmas natZ divides modulo