proposition: Lemma zlincombmodlincombmod : forall c x y n : Z, ZLinCombMod c x y n -> LinCombMod c x y (Z.abs_nat n).
proof: Proof. unfold ZLinCombMod, LinCombMod in |- *. intros. elim H. intros a Ha. exists a. elim Ha. intros b Hb. exists b. apply zmodmod. assumption. Qed.
imports: ZArith Wf_nat lemmas natZ divides modulo