proposition: Lemma scalb_correct: forall p sc b a1 p1, a1 =~~= p1 -> [[scalb sc b a1 p]] -> fst (scalb sc b a1 p) =~~= EGroup.gpow p1 pG (if b then (Pos.succ p) else p).
proof: Proof. assert (F0: forall p1, List.In p1 (FGroup.s pG)). intros p1. apply (FELLK_in pell_theory _ (in_all_znz _ p_pos)). intros p0; unfold scalb; elim p0; clear p0; fold scalb. intros p0 Hrec sc b a1 p1; case b; clear b; intros H1. generalize (Hrec sc true a1 p1 H1) (nInversible_scalb true sc a1 p0); case scalb. intros a2 sc2 H2 H3. generalize (@nedouble_correct sc2 a2) (nInversible_double sc2 a2); case ndouble. intros a3 sc3 H4 H5 H6. case (H5 H6); clear H5; intros H5 H7. simpl Pos.succ. rewrite ZCmisc.Zpos_xO_add. repeat rewrite gpow_add; auto with zarith. apply H4; auto. apply H2. inversion_clear H5; try constructor; repeat itac; auto. generalize (Hrec sc true a1 p1 H1) (nInversible_scalb true sc a1 p0); case scalb. intros a2 sc2 H2 H3. generalize (@nedouble_correct sc2 a2) (nInversible_double sc2 a2); case ndouble. intros a3 sc3 H4 H5. generalize (fun p1 p2 => (@neadd_correct sc3 (nopp a1) p1 a3 p2)) (nInversible_add sc3 (nopp a1) a3); case nadd. intros a4 sc4 H6 H7 H8. case (H7 H8); clear H7; intros H7 [H9 H10]. case H5; clear H5. inversion_clear H9; try constructor; repeat itac; auto. intros H11 H12. case H3; clear H3. inversion_clear H11; try constructor; repeat itac; auto. intros H13 H14. rewrite ZCmisc.Zpos_xI_add. replace (gpow p1 pG (p0 + p0 + 1)) with (add (opp p1) (gpow p1 pG ((Pos.succ p0) + (Pos.succ p0)))). apply H6; auto. apply nopp_correct; auto. rewrite gpow_add; auto with zarith. apply H4; auto. apply H2; auto. inversion_clear H11; try constructor; repeat itac; auto. inversion_clear H9; try constructor; repeat itac; auto. rewrite ZCmisc.Psucc_Zplus. repeat rewrite gpow_add; auto with zarith. repeat rewrite gpow_1; auto with zarith. unfold add. repeat rewrite add_assoc. apply f_equal2 with (f := SMain.add pell_theory); auto. rewrite add_comm with (p2 := p1). repeat rewrite add_assoc. unfold opp; rewrite add_opp; simpl; auto. intros p0 Hrec sc b a1 p1; case b; clear b; intros H1. generalize (Hrec sc false a1 p1 H1) (nInversible_scalb false sc a1 p0); case scalb. intros a2 sc2 H2 H3. generalize (@nedouble_correct sc2 a2) (nInversible_double sc2 a2); case ndouble. intros a3 sc3 H4 H5. generalize (fun p1 p2 => (@neadd_correct sc3 a1 p1 a3 p2)) (nInversible_add sc3 a1 a3); case nadd. intros a4 sc4 H6 H7 H8. case (H7 H8); clear H7; intros H7 [H9 H10]. case H5; clear H5. inversion_clear H9; try constructor; repeat itac; auto. intros H11 H12. case H3; clear H3. inversion_clear H11; try constructor; repeat itac; auto. intros H13 H14. simpl Pos.succ. rewrite ZCmisc.Zpos_xI_add. replace (p0 + p0 + 1)%Z with (1 + (p0 + p0))%Z; auto with zarith. repeat rewrite gpow_add; auto with zarith. repeat rewrite gpow_1; auto with zarith. apply H6; auto. apply H4; auto. apply H2; auto. inversion_clear H11; try constructor; repeat itac; auto. inversion_clear H9; try constructor; repeat itac; auto. generalize (Hrec sc false a1 p1 H1) (nInversible_scalb false sc a1 p0); case scalb. intros a2 sc2 H2 H3. generalize (@nedouble_correct sc2 a2) (nInversible_double sc2 a2); case ndouble. intros a3 sc3 H4 H5 H6. case (H5 H6); clear H5; intros H5 H7. rewrite ZCmisc.Zpos_xO_add. repeat rewrite gpow_add; auto with zarith. apply H4; auto. apply H2; auto. inversion_clear H5; try constructor; repeat itac; auto. intros sc b a1 p1 H1; case b; intros H2; simpl gpow; rewrite add_0_r; auto. apply nedouble_correct; auto. Qed.
imports: Ring Field_tac Ring_tac Eqdep_dec ZArith ZCAux Ppow GZnZ EGroup SMain Zmod