f | (n + m) = f | (n /\ (n + m)) by RELAT_1:71
.= f | n ;
hence f | (n + m) = f ; :: thesis: verum