proposition: Theorem add_le_add_left {a b : mynat} (h : a ≤ b) (t : mynat) : t + a ≤ t + b.
proof: Proof. rewrite add_comm. rewrite (add_comm t b). apply add_le_add_right. exact h. 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