Theorem Sum.Lex.inr_mono

Modification history