proposition: Lemma dadd0e_subproof : left_id (0%:dE%dE : \bar^d R) dual_adde.
proof: Proof. by case=> // r; rewrite /dual_adde /= add0r. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed