>(deg_mono … Hkl2 … Hkl1) -h -k -l2 //
| #G #L #K #V #i #l1 #HLK #_ #IHV #l2 #H
elim (da_inv_lref … H) -H * #K0 #V0 [| #l0 ] #HLK0 #HV0 [| #Hl0 ]
>(deg_mono … Hkl2 … Hkl1) -h -k -l2 //
| #G #L #K #V #i #l1 #HLK #_ #IHV #l2 #H
elim (da_inv_lref … H) -H * #K0 #V0 [| #l0 ] #HLK0 #HV0 [| #Hl0 ]