import Data.Nat

partial
test1 : (n,j,k : Nat) -> LT j k -> LT (n*j) (n*k)
test1 (S n) j k ltp =
	case ltp of
		LTESucc LTEZero =>
			-- rewrite multCommutative n 0 in
				LTESucc $ ?hole1


partial
test2 : (j,k : Nat) -> LTE j k -> LTE j k
test2 j k ltp =
	let MkUnit = ?preCase in
	case ltp of
		LTEZero => ?zeroCase
		LTESucc lteRest =>
			-- rewrite multCommutative n 0 in
				?succCase