proposition: Lemma lattice_for_lub_correct_r x y : y <= lattice_for_lub lub x y.
proof: Proof. clear lub_correct_l. destruct x as [|x|], y as [|y|]; try reflexivity. { exact (lub_correct_r x y). } { simpl. rewrite (reflexivity y : is_true (beq y y)). reflexivity. } Qed.
imports: Coq.PArith.BinPos Coq.PArith.Pnat Coq.Arith.Arith Coq.Classes.RelationClasses Coq.Classes.Morphisms Fiat.Parsers.ContextFreeGrammar.Carriers Fiat.Common.Tactics.SplitInContext Fiat.Common.Notations