proposition: Remark power_R_1 : forall a, power_R a a 1%nat.
proof: Proof. simpl; intros a; red; simpl; rewrite (Eone_right (EMonoid:=M));split. - discriminate. - reflexivity. Qed.
imports: Coq(Relations RelationClasses Lia List) Param(Param) additions(More_on_positive)