proposition: Lemma techlemma3 : forall (qlist : natlist) (a b : nat), 0 < a -> a < b -> Divides a b -> b = product qlist -> allPrime qlist -> exists qi : nat, inlist nat qi qlist /\ Divides a (multDrop qi qlist).
proof: Proof. simple induction qlist. simpl in |- *. intros. rewrite H2 in H0. elim (lt_not_le a 1). assumption. unfold lt in H. assumption. intros qi restqs IH. intros. elim (divdec a qi). intro. elim H1. intro x. intros. elim H4. intro y. intros. elim (IH y (product restqs)). intro qj. intros. elim H7. intros. split with qj. split. unfold inlist in |- *. simpl in |- *. right. assumption. rewrite H6. elim H9. intro z. intros. elim (eqdec qi qj). intro. rewrite H11. rewrite multdrop_cons_eq. rewrite <- (multdrop_mult restqs qj). split with z. rewrite mult_assoc_reverse. rewrite H10. reflexivity. assumption. intro. rewrite multdrop_cons_neq. split with z. rewrite mult_assoc_reverse. rewrite H10. reflexivity. intro. elim H11. rewrite H12. reflexivity. elim (le_or_lt y 0). intro. elim (le_lt_or_eq y 0). intro. elim (lt_n_O y). assumption. intro. rewrite H8 in H6. rewrite <- mult_n_O in H6. rewrite H6 in H. elim (lt_n_O 0). assumption. assumption. intro. assumption. apply simpl_lt_mult_l with qi. rewrite <- H6. simpl in H2. rewrite <- H2. assumption. simpl in H2. rewrite H5 in H2. rewrite H6 in H2. split with x. rewrite mult_assoc_reverse in H2. apply simpl_eq_mult_l with qi. unfold allPrime in H3. simpl in H3. elim H3. intros. elim H7. intros. apply lt_trans with 1. apply lt_O_Sn. assumption. symmetry in |- *. assumption. reflexivity. unfold allPrime in H3. simpl in H3. elim H3. intros. assumption. intros. split with qi. split. unfold inlist in |- *. simpl in |- *. left. elim (beq_nat_ok qi qi). intros. reflexivity. rewrite multdrop_cons_eq. elim H1. intros. simpl in H2. unfold Divides in |- *. unfold allPrime in H3. simpl in H3. elim H3. intros. elim (primedivmult qi a x H6). intro. elim H4. assumption. intros. elim H8. intro z. intros. split with z. rewrite H2 in H5. rewrite H9 in H5. rewrite (mult_assoc a qi) in H5. rewrite (mult_comm a) in H5. rewrite (mult_assoc_reverse qi a) in H5. apply simpl_eq_mult_l with qi. elim H6. intros. apply lt_trans with 1. apply lt_O_Sn. assumption. assumption. split with (product restqs). rewrite <- H5. assumption. Qed.
imports: Arith ZArith Wf_nat lemmas natZ dec list exp divides prime modulo gcd