proposition: Lemma psplit_correct: forall l, Pmult (fst (psplit l)) (Zmull (snd (psplit l))) = Zmullp l.
proof: Proof. assert (F1:= Pmult_assoc). assert (F2:= Pmult_comm). intros l; elim l; unfold psplit; fold psplit. simpl; auto. intros (a, n); case n. intros n1 l1; case_eq (psplit l1); simpl fst; simpl snd. intros p1 l2 Hp1 H1. rewrite Zmullp_cons; simpl fst; simpl snd. rewrite Zmull_cons; rewrite <- H1. simpl Ppow. symmetry; rewrite <- F1; rewrite (F2 a). rewrite (F2 a); repeat rewrite F1; auto. intros n1 l1; set (u := Pos.pred (xO n1)); case_eq (psplit l1); simpl fst; simpl snd. intros p1 l2 Hp1 H1. rewrite Zmullp_cons; simpl fst; simpl snd. case (Psucc_pred (xO n1)). intros HH; discriminate. intros HH; rewrite <- HH. rewrite Pplus_one_succ_l; rewrite Ppow_plus. fold u; simpl Ppow. rewrite Zmull_cons; rewrite <- H1. repeat rewrite F1. rewrite (F2 a). rewrite <- (F1 (Ppow a u)); rewrite (F2 p1). repeat rewrite F1; auto. intros l1; case_eq (psplit l1); simpl fst; simpl snd. intros p1 l2 Hp1 H1. rewrite Zmullp_cons; simpl fst; simpl snd. rewrite Zmull_cons; rewrite <- H1. simpl Ppow. repeat rewrite F1. rewrite (F2 a); auto. Qed.
imports: Ring Field_tac Ring_tac Eqdep_dec ZArith ZCAux Ppow GZnZ EGroup SMain Zmod