proposition: Theorem le_trans (a b c : mynat) (hab : a ≤ b) (hbc : b ≤ c) : a ≤ c.
proof: Proof. destruct hab as [d hab]. destruct hbc as [e hbc]. rewrite hab in hbc. exists (d + e). rewrite <- add_assoc. exact hbc. Qed.
imports: Unicode.Utf8 Game.Mynat.Definition Game.Mynat.Add Game.Mynat.Mul Game.Mynat.Le Game.World.Addition Game.World.Multiplication Game.World.Proposition Game.World.AdvancedProposition Game.World.AdvancedAddition Game.World.AdvancedMultiplication