proposition: Lemma bounded_add_var: forall i j n A, belong i A -> belong j A -> bounded A -> bounded (add_var i j n A).
proof: Proof. intros i j n A Hi Hj [Hd He]. split; auto. intros s a t Hst. apply delta_add_var in Hst as [Hst|[-> [-> ->]]]; split; auto; simpl. specialize (Hd _ _ _ Hst). destruct A. simpl. num_simpl. eapply Nat.lt_le_trans. apply Hd. apply Nat.le_max_r. specialize (Hd _ _ _ Hst). intuition. destruct A. simpl. num_simpl. apply Nat.le_max_l. destruct A. simpl. auto. 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)