proposition: Lemma nInversible_scalb: forall b sc a1 p1, [[scalb sc b a1 p1]] -> [[(a1,1%Z)]] /\ [sc].
proof: Proof. assert (F1 := N_lt_2). assert (F2: [1]). apply inversible_1; auto with zarith. intros b sc a p0; generalize sc b a; elim p0; simpl; auto; clear sc b a p0. intros p0 Hrec sc b a. generalize (Hrec sc true a). case scalb. intros a1 sc1 H; case b; intros H1; try apply H; clear b H. case (nInversible_double sc1 a1 H1); auto; clear H1. intros H2 H3; inversion_clear H2; try constructor; repeat itac; auto. generalize H1 (nInversible_double sc1 a1); case ndouble. intros a2 sc2 H2 H3; case H3. generalize (nInversible_add sc2 (nopp a) a2 H2). intros H4; case H4; intros _ [H5 H6]. inversion_clear H5; constructor; repeat itac; auto. intros H4; inversion_clear H4; constructor; repeat itac; auto. intros p0 Hrec sc b a. generalize (Hrec sc false a). case scalb. intros a1 sc1 H; case b; intros H1; try apply H; clear b H. generalize H1 (nInversible_double sc1 a1); case ndouble. intros a2 sc2 H2 H3; case H3. generalize (nInversible_add sc2 a a2 H2). intros H4; case H4; intros _ [H5 H6]. inversion_clear H5; constructor; repeat itac; auto. intros H4; inversion_clear H4; constructor; repeat itac; auto. case (nInversible_double sc1 a1 H1); auto; clear H1. intros H2 H3; inversion_clear H2; try constructor; repeat itac; auto. intros sc b a; case b; intros H. case (nInversible_double _ _ H); auto; clear H. inversion_clear H; split; try constructor; repeat itac; auto. Qed.
imports: Ring Field_tac Ring_tac Eqdep_dec ZArith ZCAux Ppow GZnZ EGroup SMain Zmod