proposition: Lemma alllincombzalllincomb : forall (a n m : Z) (qlist : Zlist), (0 <= n)%Z -> (0 <= m)%Z -> allPos qlist -> ZallLinCombMod a n m n qlist -> allLinCombMod a (Z.abs_nat n) (Z.abs_nat m) (map _ _ Z.abs_nat qlist).
proof: Proof. intros. unfold ZallLinCombMod in H. elim (alllist_ok Z (fun q : Z => ZLinCombMod 1 (ZExp a (m * zmultDrop q qlist) - 1) n n) qlist). intros. elim (alllist_ok nat (fun q0 : nat => LinCombMod 1 (Exp a (Z.abs_nat m * multDrop q0 (map _ _ Z.abs_nat qlist)) - 1) (Z_of_nat (Z.abs_nat n)) (Z.abs_nat n)) (map _ _ Z.abs_nat qlist)). intros. apply H6. intros. rewrite <- inj_zexp. rewrite Znat.inj_mult. rewrite inj_abs_pos. rewrite inj_abs_pos. replace m with (Z_of_nat (Z.abs_nat m)). rewrite <- Znat.inj_mult. apply zlincombmodlincombmod. rewrite Znat.inj_mult. rewrite inj_abs_pos. rewrite multdropzmultdrop. rewrite inj_abs_pos_list. apply H3. assumption. apply inlist_inj_abs_pos_list. assumption. assumption. assumption. apply Z.le_ge. assumption. apply inj_abs_pos. apply Z.le_ge. assumption. apply Z.le_ge. assumption. apply Z.le_ge. assumption. Qed.
imports: Arith ZArith lemmas natZ dec list exp divides prime modulo gcd modprime order