proposition: Lemma below_max_pi1: forall n m m', below n m' -> below (pi1 n) (max (pi0 m) (pi1 m')).
proof: Proof. intros. rewrite lt_nat_spec, max_spec. eapply Nat.lt_le_trans. 2: apply Nat.le_max_r. rewrite <- lt_nat_spec. apply lt_pi1. assumption. 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)