proposition: Theorem add_shift_minus: forall p1 p2 p3, add p1 p2 = p3 -> p1 = add p3 (opp p2).
proof: Proof. intros p1 p2 p3 H. apply cancel with (opp (opp p2)). repeat rewrite (add_comm (opp (opp p2))). rewrite add_minus_id; rewrite opp_opp; auto. Qed.
imports: Arith_base Field_tac Ring Eqdep_dec FGroup List UList ZArith