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