proposition: Lemma nInversible_double: forall sc x, [[ndouble sc x]] -> [[(x,1%Z)]] /\ [sc].
proof: Proof. assert (F1 := N_lt_2). assert (F2: inversible N 1). apply inversible_1; auto with zarith. unfold ndouble; intros sc x; case x; auto. intros H; inversion_clear H. repeat split; auto; try constructor; auto. intros x1 y1 z1; case Zeq_bool; auto. intros H; inversion_clear H. repeat split; auto; try constructor; auto; repeat itac. intros H; inversion_clear H; auto. repeat split; auto; try constructor; repeat itac; auto. Qed.
imports: Ring Field_tac Ring_tac Eqdep_dec ZArith ZCAux Ppow GZnZ EGroup SMain Zmod