∀ f g n m, n ≤ m ⇒ sameF_upto m f g ⇒ sameF_upto n f g

Theorem sameF_upto_le : forall A, forall (f:(nat.nat -> A)), forall (g:(nat.nat -> A)), forall (n:nat.nat), forall (m:nat.nat), (nat.le n m) -> (sameF_upto (A) m f g) -> sameF_upto (A) n f g.

theorem sameF_upto_le : \forall A. \forall (f:nat -> A). \forall (g:nat -> A). \forall (n:nat). \forall (m:nat). ((le) n m) -> ((sameF_upto) (A) m f g) -> (sameF_upto) (A) n f g.

theorem sameF_upto_le : forall (A : Type) , forall (f:(nat.nat) -> A) , forall (g:(nat.nat) -> A) , forall (n:nat.nat) , forall (m:nat.nat) , ((((nat.le_) ) (n)) (m)) -> (((((bigops.sameF_upto) (A)) (m)) (f)) (g)) -> ((((bigops.sameF_upto) (A)) (n)) (f)) (g).

sameF_upto_le [A:TYPE+] : LEMMA (FORALL(f:[nat_sttfa_th.sttfa_nat -> A]):(FORALL(g:[nat_sttfa_th.sttfa_nat -> A]):(FORALL(n:nat_sttfa_th.sttfa_nat):(FORALL(m:nat_sttfa_th.sttfa_nat):(nat_sttfa_th.le(n)(m) => (bigops_sttfa.sameF_upto[A](m)(f)(g) => bigops_sttfa.sameF_upto[A](n)(f)(g)))))))

Printing for OpenTheory is not working at the moment.