theorem thm1 {L : Type u_1} {M : Type u_2} [CompleteLattice L] [CompleteLattice M] {alpha : L → M} {gamma : M → L} (gc : GaloisConnection alpha gamma) {F : L → L} {G : M → M} (_F_mon : monotone F) (G_mon : monotone G) (h : ∀ (x : M), Poset.le (alpha (F (gamma x))) (G x)) : Poset.le (alpha (lfp F)) (lfp G)

theorem thm2 {L : Type u_1} {M : Type u_2} [instL : CompleteLattice L] [instM : CompleteLattice M] {alpha : L → M} {gamma : M → L} (gc : GaloisConnection alpha gamma) {F : L → L} {G : M → M} (F_mon : monotone F) (G_mon : monotone G) (h : ∀ (x : M), Poset.le (G x) (alpha (F (gamma x)))) : Poset.le (gfp G) (alpha (gfp F))