proposition: Corollary kat_complete_leq n m: forall e f: gregex n m, G e ≦ G f -> e ≦ f.
proof: Proof. intros e f. rewrite 2leq_iff_cup, <-G.lang_pls. apply kat_complete_weq. Qed.
imports: Coq.PArith.BinPosDef denum lset sums normalisation kat ka_completeness untyping regex gregex lsyntax syntax lang glang boolean atoms