proposition: Lemma gen_point {Hl: CNV+TOP ≪ l} n m k (p: X n m): is_nonempty' k -> is_point p -> is_point (p⋅top' m k).
proof: Proof. intros Hk Hp. split. unfold is_vector. now mrewrite top_mnn. unfold is_injective. ra_normalise. mrewrite (leq_xt (top' m k ⋅ top' k m)). mrewrite vector. apply injective. intros i j. mrewrite (top_nonempty (n:=m) (m:=k) (p:=j)). apply nonempty. Qed.
imports: common lattice monoid kleene normalisation rewriting