proposition: Theorem add_opp: forall p, add p (opp p) = inf_elt.
proof: Proof. intros p; case p; unfold add; simpl; auto. intros x1 y1 H1. repeat ksplit. case KD0; ring. Qed.
imports: Arith_base Field_tac Ring Eqdep_dec FGroup List UList ZArith