proposition: Lemma AMField : field_theory zeroAM unAM plusAM multAM minusAM oppAM divAM invAM(eq(A:=AM)).
proof: Proof. constructor. apply AM_theory. rewrite <- fR1 in |- *; apply nonzeroAM; discrR. reflexivity. exact invAM_l. Qed.