- [* // #a #tl #_ #H @False_ind @(absurd (a < 0))
- [@H %1 % | @le_to_not_lt //]
- |#m #Hind #l #Huni #Hmem <(filter_length2 ? (eqb m) l)
- lapply (length_filter_eqb … m l Huni) #Hle
- @(transitive_le ? (1+|filter ? (λx.¬ eqb m x) l|))
- [@le_plus //
- |@le_S_S @Hind
- [@unique_filter //
- |#x #memx cut (x ≤ m)
- [@le_S_S_to_le @Hmem @(mem_filter … memx)] #Hcut
- cases(le_to_or_lt_eq … Hcut) // #eqxm @False_ind
- @(absurd ? eqxm) @sym_not_eq @eqb_false_to_not_eq
- @injective_notb @(mem_filter_true ???? memx)
+ [* // #a #tl #_ #H @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 @(\ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6 (a \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6))
+ [@H %1 % | @\ 5a href="cic:/matita/arithmetics/nat/le_to_not_lt.def(8)"\ 6le_to_not_lt\ 5/a\ 6 //]
+ |#m #Hind #l #Huni #Hmem <(\ 5a href="cic:/matita/basics/lists/search/filter_length2.def(5)"\ 6filter_length2\ 5/a\ 6 ? (\ 5a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"\ 6eqb\ 5/a\ 6 m) l)
+ lapply (\ 5a href="cic:/matita/basics/lists/search/length_filter_eqb.def(8)"\ 6length_filter_eqb\ 5/a\ 6 … m l Huni) #Hle
+ @(\ 5a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"\ 6transitive_le\ 5/a\ 6 ? (\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 61\ 5/a\ 6\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6|\ 5a href="cic:/matita/basics/lists/search/filter.def(2)"\ 6filter\ 5/a\ 6 ? (λx.\ 5a title="boolean not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"\ 6eqb\ 5/a\ 6 m x) l\ 5a title="list length" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6))
+ [@\ 5a href="cic:/matita/arithmetics/nat/le_plus.def(7)"\ 6le_plus\ 5/a\ 6 //
+ |@\ 5a href="cic:/matita/arithmetics/nat/le_S_S.def(2)"\ 6le_S_S\ 5/a\ 6 @Hind
+ [@\ 5a href="cic:/matita/basics/lists/search/unique_filter.def(4)"\ 6unique_filter\ 5/a\ 6 //
+ |#x #memx cut (x \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 m)
+ [@\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"\ 6le_S_S_to_le\ 5/a\ 6 @Hmem @(\ 5a href="cic:/matita/basics/lists/search/mem_filter.def(3)"\ 6mem_filter\ 5/a\ 6 … memx)] #Hcut
+ cases(\ 5a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"\ 6le_to_or_lt_eq\ 5/a\ 6 … Hcut) // #eqxm @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6
+ @(\ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6 ? eqxm) @\ 5a href="cic:/matita/basics/logic/sym_not_eq.def(4)"\ 6sym_not_eq\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/nat/eqb_false_to_not_eq.def(6)"\ 6eqb_false_to_not_eq\ 5/a\ 6
+ @\ 5a href="cic:/matita/basics/bool/injective_notb.def(4)"\ 6injective_notb\ 5/a\ 6 @(\ 5a href="cic:/matita/basics/lists/search/mem_filter_true.def(4)"\ 6mem_filter_true\ 5/a\ 6 ???? memx)