proposition: Lemma Psub_ok P' P l : (P -- P')@l == P@l - P'@l.
proof: Proof. revert P l; induction P' as [|p P' IHP'|? IHP'1 ? ? IHP'2];simpl;intros P l;Esimpl. - revert p l; induction P as [|? ? IHP|? IHP1 ? ? IHP2];simpl;intros p0 l. + Esimpl; add_permut. + destr_pos_sub; intros ->;Esimpl. * rewrite IHP';rsimpl. * rewrite IHP';Esimpl. now rewrite Pjump_add. * rewrite IHP. now rewrite Pjump_add. + destruct p0;simpl. * rewrite IHP2;simpl. rsimpl. rewrite Pjump_xO_tail. Esimpl. * rewrite IHP2;simpl. rewrite Pjump_pred_double. rsimpl. * rewrite IHP'. rsimpl. - destruct P as [|p0|];simpl. + Esimpl; add_permut. + destruct p0;simpl;Esimpl; rewrite IHP'2; simpl. * rewrite Pjump_xO_tail. rsimpl. add_permut. * rewrite Pjump_pred_double. rsimpl. add_permut. * rsimpl. unfold tail. add_permut. + destr_pos_sub; intros ->; Esimpl. * rewrite IHP'1, IHP'2;rsimpl. add_permut. * rewrite IHP'1, IHP'2;simpl;Esimpl. rewrite pow_pos_add;rsimpl. add_permut. * rewrite PsubX_ok by trivial;rsimpl. rewrite IHP'2, pow_pos_add;rsimpl. add_permut. Qed.
imports: Setoid Morphisms Env BinPos BinNat BinInt Ring_theory