proposition: Lemma leq_card e e': e ≦ e' -> #|e| <= #|e'|.
proof: Proof. move => A. apply: subset_leq_card. apply/subsetP => x. exact: A. Qed.
imports: Setoid Morphisms kat normalisation rewriting kat_tac comparisons rel relalg boolean mathcomp(all_ssreflect)