proposition: Lemma sigma2_strictly_positive : forall (x y : Site) (l1 l2 : list Site), In x l1 -> In y l2 -> (forall x' y' : Site, (f x' y' (t x' y') >= 0)%Z) -> (f x y (t x y) > 0)%Z -> (sigma2_table Site l1 l2 Data f t > 0)%Z.
proof: Proof. unfold sigma2_table in |- *. intros x y l1 l2 H H0 H1 H2. unfold sigma_table in |- *. apply sigma_strictly_positive with (x := x). auto. auto. intro y0. unfold Z_id in |- *. apply sigma_pos. intro x_. generalize (H1 y0 x_). auto. unfold Z_id in |- *. apply sigma_strictly_positive with (x := y). auto. auto. intro y0. generalize (H1 x y0). auto. auto. Qed.
imports: List fifo table reduce