proposition: Lemma labelling_crop : forall n A i j, bounded A -> max_label A <= n -> labelling (max_label A) (fun a => deltabrel A i a j) == labelling n (fun a => deltabrel A i a j).
proof: Proof. intros n A i j HA H. induction H. reflexivity. rewrite IHle. rewrite labelling_S. case_eq (deltabrel A i (num_of_nat m) j); intro Hij. apply HA in Hij. num_lia_false. unfold xif. semiring_reflexivity. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(SemiRing) ATBR(KleeneAlgebra) ATBR(MxGraph) ATBR(MxSemiLattice) ATBR(MxSemiRing) ATBR(MxKleeneAlgebra) ATBR(DKA_Definitions) ATBR(DKA_CheckLabels) ATBR(StrictStarForm) ATBR(Utils_WF) Coq(Relations)