∀c:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 c → \ 5a href="cic:/matita/basics/relations/monotonic.def(1)"\ 6monotonic\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/lt.def(1)"\ 6lt\ 5/a\ 6 (λt.(c\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6t)).
#c #posc #n #m #ltnm
(elim ltnm) normalize
- [/\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/monotonic_lt_plus_l.def(9)"\ 6monotonic_lt_plus_l\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+ [/\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/monotonic_lt_plus_l.def(5)"\ 6monotonic_lt_plus_l\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
|#a #_ #lt1 @(\ 5a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"\ 6transitive_le\ 5/a\ 6 … lt1) //
]
qed.
theorem monotonic_lt_times_l:
∀c:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 c → \ 5a href="cic:/matita/basics/relations/monotonic.def(1)"\ 6monotonic\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/lt.def(1)"\ 6lt\ 5/a\ 6 (λt.(t\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6c)).
-/\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/monotonic_lt_times_r.def(10)"\ 6monotonic_lt_times_r\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+/\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/monotonic_lt_times_r.def(9)"\ 6monotonic_lt_times_r\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
qed.
theorem lt_to_le_to_lt_times:
#n #m #p #q #ltnm #lepq #posq
@(\ 5a href="cic:/matita/arithmetics/nat/le_to_lt_to_lt.def(4)"\ 6le_to_lt_to_lt\ 5/a\ 6 ? (n\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6q))
[@\ 5a href="cic:/matita/arithmetics/nat/monotonic_le_times_r.def(8)"\ 6monotonic_le_times_r\ 5/a\ 6 //
- |@\ 5a href="cic:/matita/arithmetics/nat/monotonic_lt_times_l.def(11)"\ 6monotonic_lt_times_l\ 5/a\ 6 //
+ |@\ 5a href="cic:/matita/arithmetics/nat/monotonic_lt_times_l.def(10)"\ 6monotonic_lt_times_l\ 5/a\ 6 //
]
qed.
theorem le_minus_to_plus: ∀n,m,p. n\ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6m \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 p → n\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 p\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6m.
#n #m #p #lep @\ 5a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"\ 6transitive_le\ 5/a\ 6
- [|@\ 5a href="cic:/matita/arithmetics/nat/le_plus_minus_m_m.def(9)"\ 6le_plus_minus_m_m\ 5/a\ 6 | @\ 5a href="cic:/matita/arithmetics/nat/monotonic_le_plus_l.def(6)"\ 6monotonic_le_plus_l\ 5/a\ 6 // ]
+ [|@\ 5a href="cic:/matita/arithmetics/nat/le_plus_minus_m_m.def(6)"\ 6le_plus_minus_m_m\ 5/a\ 6 | @\ 5a href="cic:/matita/arithmetics/nat/monotonic_le_plus_l.def(6)"\ 6monotonic_le_plus_l\ 5/a\ 6 // ]
qed.
theorem le_minus_to_plus_r: ∀a,b,c. c \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 b → a \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 b \ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6 c → a \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 c \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 b.
theorem lt_minus_to_plus: ∀a,b,c. a \ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6 b \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 c → a \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 c \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 b.
#a #b #c #H @\ 5a href="cic:/matita/arithmetics/nat/not_le_to_lt.def(5)"\ 6not_le_to_lt\ 5/a\ 6
-@(\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6 … (\ 5a href="cic:/matita/arithmetics/nat/lt_to_not_le.def(7)"\ 6lt_to_not_le\ 5/a\ 6 …H)) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/le_plus_to_minus_r.def(10)"\ 6le_plus_to_minus_r\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+@(\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6 … (\ 5a href="cic:/matita/arithmetics/nat/lt_to_not_le.def(7)"\ 6lt_to_not_le\ 5/a\ 6 …H)) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/le_plus_to_minus_r.def(7)"\ 6le_plus_to_minus_r\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
qed.
theorem lt_minus_to_plus_r: ∀a,b,c. a \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 b \ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6 c → a \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 c \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 b.
qed.
theorem lt_plus_to_minus_r: ∀a,b,c. a \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 b \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 c → a \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 c \ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6 b.
-#a #b #c #H @\ 5a href="cic:/matita/arithmetics/nat/le_plus_to_minus_r.def(10)"\ 6le_plus_to_minus_r\ 5/a\ 6 //
+#a #b #c #H @\ 5a href="cic:/matita/arithmetics/nat/le_plus_to_minus_r.def(7)"\ 6le_plus_to_minus_r\ 5/a\ 6 //
qed.
theorem monotonic_le_minus_r:
projects / helm.git / blobdiff