lapply (le_plus_to_minus … Hd21) -Hd21 #Hd21 /3 width=5/
| -Hd21 normalize in Hde12;
lapply (lt_to_le_to_lt 0 … Hde12) // #He2
lapply (le_plus_to_minus … Hd21) -Hd21 #Hd21 /3 width=5/
| -Hd21 normalize in Hde12;
lapply (lt_to_le_to_lt 0 … Hde12) // #He2