proposition: Theorem divA_nZ : forall a b : A, ~ eqA b A0 -> forall nZa : ~ eqA a A0, ~ eqA (divA b a nZa) A0.
proof: Proof. Proof using plusA multA minusA invA cs A1. intros a b H' nZa; red in |- *; intros H'1; auto. case H'; apply (eqA_trans _ _ _ _ _ _ _ _ _ cs) with (y := multA (divA b a nZa) a); auto. apply divA_is_multA with (1 := cs); auto. apply (eqA_trans _ _ _ _ _ _ _ _ _ cs) with (y := multA A0 a); auto. apply multA_eqA_comp with (1 := cs); auto. apply (eqA_ref _ _ _ _ _ _ _ _ _ cs); auto. apply multA_A0_l with (1 := cs); auto. Qed.
imports: Buchberger(moreCoefStructure)