proposition: Lemma covers_dual x y : covers (T := T^d) y x = covers x y.
proof: Proof. rewrite /= ltEdual; congr (_ && _); apply: eq_forallb => z. by rewrite !ltEdual andbC. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(order) tools