proposition: Lemma pow_pos_add x i j : x^(j + i) == x^i * x^j.
proof: Proof. rewrite Pos.add_comm. apply (pow_pos_add Rsth (Rmul_ext Reqe) (ARmul_assoc ARth)). Qed.
imports: Setoid Morphisms BinList BinPos BinNat BinInt Ring_theory