proposition: Lemma Psub_opp P' P : P -- P' === P ++ (--P').
proof: Proof. revert P; induction P' as [|p P' IHP'|P'1 IHP'1 p P'2 IHP'2]; simpl; intros P. - intro l; Esimpl. - revert p; induction P; simpl; intros p0; try reflexivity. + destr_pos_sub; intros ->; now apply mkPinj_ext. + destruct p0; now apply PX_ext. - destruct P as [|p0 P|P2 p0 P3]; simpl; try reflexivity. + destruct p0; now apply PX_ext. + destr_pos_sub; intros ->; apply mkPX_ext; auto. let p1 := match goal with |- PsubX _ _ ?p1 _ === _ => p1 end in revert p1. induction P2; simpl; intros; try reflexivity. destr_pos_sub; intros ->; now apply mkPX_ext. Qed.
imports: Setoid Morphisms BinList BinPos BinNat BinInt Ring_theory