proposition: Lemma leq_destruct_plus: forall (x y z: X A B), x+y <== z -> x<==z /\ y<==z.
proof: Proof. intros x y z H; rewrite <- H; split; unfold leq. rewrite plus_assoc, plus_idem. reflexivity. rewrite (plus_com x), plus_assoc, plus_idem. reflexivity. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph)