proposition: Theorem le_antisymm (a b : mynat) (hab : a ≤ b) (hba : b ≤ a) : a = b.
proof: Proof. destruct hab as [c hab]. destruct hba as [d hba]. rewrite hab in hba. rewrite add_assoc in hba. symmetry in hba. apply eq_zero_of_add_right_eq_self in hba. rewrite add_comm in hba. apply add_left_eq_zero in hba. rewrite hba in hab. symmetry in hab. exact hab. 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