proposition: Lemma nInversible_scal_list: forall sc a l, [[scal_list sc a l]] -> [[(a,1%Z)]] /\ [sc].
proof: Proof. assert (F1 := N_lt_2). assert (F2: [1]). apply inversible_1; auto with zarith. intros sc a l; generalize sc a; unfold scal; elim l; simpl; auto; clear sc a l. intros sc a; unfold scal_list; simpl. intros HH; inversion_clear HH; split; auto; try constructor; repeat itac; auto. intros n1 l1 Hrec sc a. unfold scal_list; simpl. generalize (nInversible_scal sc a n1). case scal. intros n z H1 H2. case (Hrec _ _ H2). intros H3 H4; apply H1; auto. inversion_clear H3; constructor; repeat itac; auto. Qed.
imports: Ring Field_tac Ring_tac Eqdep_dec ZArith ZCAux Ppow GZnZ EGroup SMain Zmod