proposition: Lemma Padd_ok P' P l : (P ++ P')@l == P@l + P'@l.
proof: Proof. revert P l; induction P' as [|p P' IHP'|P'1 IHP'1 p P'2 IHP'2]; simpl;intros P l;Esimpl. - revert p l; induction P as [|p P IHP|P2 IHP1 p P3 IHP2];simpl;intros p0 l. + Esimpl; add_permut. + destr_pos_sub; intros ->;Esimpl. * now rewrite IHP'. * rewrite IHP';Esimpl. now rewrite jump_add'. * rewrite IHP. now rewrite jump_add'. + destruct p0;simpl. * rewrite IHP2;simpl. rsimpl. * rewrite IHP2;simpl. rewrite jump_pred_double. rsimpl. * rewrite IHP'. rsimpl. - destruct P as [|p0 ?|? ? ?];simpl. + Esimpl. add_permut. + destruct p0;simpl;Esimpl; rewrite IHP'2; simpl. * rsimpl. add_permut. * rewrite jump_pred_double. rsimpl. add_permut. * rsimpl. 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 PaddX_ok by trivial; rsimpl. rewrite IHP'2, pow_pos_add; rsimpl. add_permut. Qed.
imports: Setoid Morphisms BinList BinPos BinNat BinInt Ring_theory